Basic

📁 Source: Mathlib/Combinatorics/Digraph/Basic.lean

Statistics

Metric	Count
Definitions `Digraph`, `adjDecidable`, `adjDecidable`, `adjDecidable`, `IsSubgraph`, `adjDecidable`, `adjDecidable`, `adjDecidable`, `completeAtomicBooleanAlgebra`, `completeBipartiteGraph`, `completeDigraph`, `distribLattice`, `emptyDigraph`, `infSet`, `instCompl`, `instInhabited`, `instLE`, `instMax`, `instMin`, `instPartialOrder`, `instUniqueOfIsEmpty`, `mk'`, `sdiff`, `supSet`, `instDecidableRelAdjCoeEmbeddingForallForallBoolDigraphMk'`, `instFintypeDigraphOfDecidableEq`	26
Theorems `adj_inj`, `adj_injective`, `bot_adj`, `compl_adj`, `completeBipartiteGraph_Adj`, `completeDigraph_eq_top`, `default_def`, `emptyDigraph_eq_bot`, `ext`, `ext_iff`, `iInf_adj`, `iSup_adj`, `inf_adj`, `instNontrivialOfNonempty`, `isSubgraph_eq_le`, `mk'_apply_Adj`, `sInf_adj`, `sSup_adj`, `sdiff_adj`, `sup_adj`, `top_adj`	21
Total	47

Digraph

Definitions

Name	Category	Theorems
`IsSubgraph` 📖	MathDef	1 math math: `isSubgraph_eq_le`
`completeAtomicBooleanAlgebra` 📖	CompOp	9 math math: `default_def`, `bot_adj`, `toSimpleGraphStrict_top`, `toSimpleGraphInclusive_bot`, `top_adj`, `completeDigraph_eq_top`, `toSimpleGraphInclusive_top`, `toSimpleGraphStrict_bot`, `emptyDigraph_eq_bot`
`completeBipartiteGraph` 📖	CompOp	1 math math: `completeBipartiteGraph_Adj`
`completeDigraph` 📖	CompOp	1 math math: `completeDigraph_eq_top`
`distribLattice` 📖	CompOp	—
`emptyDigraph` 📖	CompOp	1 math math: `emptyDigraph_eq_bot`
`infSet` 📖	CompOp	2 math math: `sInf_adj`, `iInf_adj`
`instCompl` 📖	CompOp	1 math math: `compl_adj`
`instInhabited` 📖	CompOp	1 math math: `default_def`
`instLE` 📖	CompOp	1 math math: `isSubgraph_eq_le`
`instMax` 📖	CompOp	1 math math: `sup_adj`
`instMin` 📖	CompOp	1 math math: `inf_adj`
`instPartialOrder` 📖	CompOp	2 math math: `toSimpleGraphStrict_mono`, `toSimpleGraphInclusive_mono`
`instUniqueOfIsEmpty` 📖	CompOp	—
`mk'` 📖	CompOp	1 math math: `mk'_apply_Adj`
`sdiff` 📖	CompOp	1 math math: `sdiff_adj`
`supSet` 📖	CompOp	2 math math: `iSup_adj`, `sSup_adj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_inj` 📖	mathematical	—	`Adj`	—	`ext_iff`
`adj_injective` 📖	mathematical	—	`Digraph` `Adj`	—	`ext`
`bot_adj` 📖	mathematical	—	`Adj` `Bot.bot` `Digraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`compl_adj` 📖	mathematical	—	`Adj` `Compl.compl` `Digraph` `instCompl`	—	—
`completeBipartiteGraph_Adj` 📖	mathematical	—	`Adj` `completeBipartiteGraph`	—	—
`completeDigraph_eq_top` 📖	mathematical	—	`completeDigraph` `Top.top` `Digraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`default_def` 📖	mathematical	—	`Digraph` `instInhabited` `Bot.bot` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`emptyDigraph_eq_bot` 📖	mathematical	—	`emptyDigraph` `Bot.bot` `Digraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`ext` 📖	—	`Adj`	—	—	—
`ext_iff` 📖	mathematical	—	`Adj`	—	`ext`
`iInf_adj` 📖	mathematical	—	`Adj` `iInf` `Digraph` `infSet`	—	—
`iSup_adj` 📖	mathematical	—	`Adj` `iSup` `Digraph` `supSet`	—	—
`inf_adj` 📖	mathematical	—	`Adj` `Digraph` `instMin`	—	—
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `Digraph`	—	—
`isSubgraph_eq_le` 📖	mathematical	—	`IsSubgraph` `Digraph` `instLE`	—	—
`mk'_apply_Adj` 📖	mathematical	—	`Adj` `DFunLike.coe` `Function.Embedding` `Digraph` `Function.instFunLikeEmbedding` `mk'`	—	—
`sInf_adj` 📖	mathematical	—	`Adj` `InfSet.sInf` `Digraph` `infSet`	—	—
`sSup_adj` 📖	mathematical	—	`Adj` `SupSet.sSup` `Digraph` `supSet` `Set` `Set.instMembership`	—	—
`sdiff_adj` 📖	mathematical	—	`Adj` `Digraph` `sdiff`	—	—
`sup_adj` 📖	mathematical	—	`Adj` `Digraph` `instMax`	—	—
`top_adj` 📖	mathematical	—	`Adj` `Top.top` `Digraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—

Digraph.Bot

Definitions

Name	Category	Theorems
`adjDecidable` 📖	CompOp	—

Digraph.Compl

Definitions

Name	Category	Theorems
`adjDecidable` 📖	CompOp	—

Digraph.Inf

Definitions

Name	Category	Theorems
`adjDecidable` 📖	CompOp	—

Digraph.SDiff

Definitions

Name	Category	Theorems
`adjDecidable` 📖	CompOp	—

Digraph.Sup

Definitions

Name	Category	Theorems
`adjDecidable` 📖	CompOp	—

Digraph.Top

Definitions

Name	Category	Theorems
`adjDecidable` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Digraph` 📖	CompData	23 math math: `Digraph.default_def`, `Digraph.sup_adj`, `Digraph.bot_adj`, `Digraph.toSimpleGraphStrict_top`, `Digraph.inf_adj`, `Digraph.toSimpleGraphStrict_mono`, `Digraph.sdiff_adj`, `Digraph.iSup_adj`, `Digraph.toSimpleGraphInclusive_bot`, `Digraph.top_adj`, `Digraph.sInf_adj`, `Digraph.sSup_adj`, `Digraph.compl_adj`, `Digraph.toSimpleGraphInclusive_mono`, `Digraph.completeDigraph_eq_top`, `Digraph.isSubgraph_eq_le`, `Digraph.toSimpleGraphInclusive_top`, `Digraph.toSimpleGraphStrict_bot`, `Digraph.adj_injective`, `Digraph.emptyDigraph_eq_bot`, `Digraph.iInf_adj`, `Digraph.mk'_apply_Adj`, `Digraph.instNontrivialOfNonempty`
`instDecidableRelAdjCoeEmbeddingForallForallBoolDigraphMk'` 📖	CompOp	—
`instFintypeDigraphOfDecidableEq` 📖	CompOp	—

---

← Back to Index