Documentation Verification Report

Basic

📁 Source: Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean

Statistics

Metric	Count
Definitions `IsExtremal`, `extremalNumber`	2
Theorems `extremalNumber_le`, `of_extremalNumber_lt_card_edgeFinset`, `le_iff_eq`, `prop`, `card_edgeFinset_deleteIncidenceSet_le_extremalNumber`, `card_edgeFinset_le_extremalNumber`, `card_edgeFinset_of_isExtremal_free`, `exists_isExtremal_free`, `exists_isExtremal_iff_exists`, `extremalNumber_congr`, `extremalNumber_congr_right`, `extremalNumber_le_iff`, `extremalNumber_le_iff_of_nonneg`, `extremalNumber_of_fintypeCard_eq`, `isExtremal_free_iff`, `lt_extremalNumber_iff`, `lt_extremalNumber_iff_of_nonneg`	17
Total	19

SimpleGraph

Definitions

Name	Category	Theorems
`IsExtremal` 📖	MathDef	5 math math: `isExtremal_top_free_iff_isTuranMaximal`, `isExtremal_free_iff`, `isExtremal_top_free_turanGraph`, `exists_isExtremal_iff_exists`, `exists_isExtremal_free`
`extremalNumber` 📖	CompOp	17 math math: `extremalNumber_congr`, `extremalNumber_le_iff_of_nonneg`, `antitoneOn_extremalNumber_div_choose_two`, `extremalNumber_congr_right`, `card_edgeFinset_of_isExtremal_free`, `card_edgeFinset_le_extremalNumber`, `isExtremal_free_iff`, `extremalNumber_top`, `card_edgeFinset_deleteIncidenceSet_le_extremalNumber`, `IsContained.extremalNumber_le`, `extremalNumber_of_fintypeCard_eq`, `tendsto_turanDensity`, `extremalNumber_le_iff`, `lt_extremalNumber_iff`, `lt_extremalNumber_iff_of_nonneg`, `isEquivalent_extremalNumber`, `card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_edgeFinset_deleteIncidenceSet_le_extremalNumber` 📖	mathematical	`Free`	`Finset.card` `Sym2` `edgeFinset` `deleteIncidenceSet` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjDeleteIncidenceSet` `extremalNumber` `Fintype.card`	—	`card_edgeFinset_induce_compl_singleton` `Fintype.card_unique` `Fintype.card_compl_set` `card_edgeFinset_le_extremalNumber` `Mathlib.Tactic.Contrapose.contrapose₄` `IsContained.trans`
`card_edgeFinset_le_extremalNumber` 📖	mathematical	`Free`	`Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `extremalNumber` `Fintype.card`	—	`extremalNumber_of_fintypeCard_eq` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Finset.le_sup`
`card_edgeFinset_of_isExtremal_free` 📖	mathematical	`IsExtremal` `Free`	`Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `extremalNumber` `Fintype.card`	—	`isExtremal_free_iff`
`exists_isExtremal_free` 📖	mathematical	—	`IsExtremal` `Free`	—	`exists_isExtremal_iff_exists` `free_bot`
`exists_isExtremal_iff_exists` 📖	mathematical	—	`IsExtremal`	—	`Finset.exists_max_image` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton`
`extremalNumber_congr` 📖	mathematical	—	`extremalNumber`	—	`le_antisymm_iff` `Fintype.card_fin` `extremalNumber_le_iff` `card_edgeFinset_le_extremalNumber` `Mathlib.Tactic.Contrapose.contrapose₄` `IsContained.trans'`
`extremalNumber_congr_right` 📖	mathematical	—	`extremalNumber`	—	`extremalNumber_congr`
`extremalNumber_le_iff` 📖	mathematical	—	`extremalNumber` `Fintype.card` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`extremalNumber_of_fintypeCard_eq` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton`
`extremalNumber_le_iff_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `extremalNumber` `Fintype.card` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`Nat.le_floor_iff` `extremalNumber_le_iff`
`extremalNumber_of_fintypeCard_eq` 📖	mathematical	`Fintype.card`	`extremalNumber` `Finset.sup` `SimpleGraph` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeNat` `Nat.instOrderBot` `Finset.filter` `Free` `IsContained` `Finset.univ` `instFintypeSimpleGraphOfDecidableEq` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `Adj`	—	`extremalNumber.eq_1` `le_antisymm_iff` `Finset.sup_le_iff` `Finset.mem_filter` `free_congr` `Finset.filter.congr_simp` `Iso.card_edgeFinset_eq` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Finset.le_sup`
`isExtremal_free_iff` 📖	mathematical	—	`IsExtremal` `Free` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `extremalNumber` `Fintype.card`	—	`IsExtremal.eq_1` `extremalNumber_le_iff` `eq_of_le_of_ge` `card_edgeFinset_le_extremalNumber` `ge_of_eq`
`lt_extremalNumber_iff` 📖	mathematical	—	`extremalNumber` `Fintype.card` `Free` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`extremalNumber_of_fintypeCard_eq` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton`
`lt_extremalNumber_iff_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Preorder.toLT` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `extremalNumber` `Fintype.card` `Free` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`Nat.floor_lt` `lt_extremalNumber_iff`

SimpleGraph.IsContained

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extremalNumber_le` 📖	mathematical	—	`SimpleGraph.extremalNumber`	—	`Fintype.card_fin` `SimpleGraph.extremalNumber_le_iff` `Mathlib.Tactic.Contrapose.contrapose₂` `trans` `of_extremalNumber_lt_card_edgeFinset`
`of_extremalNumber_lt_card_edgeFinset` 📖	mathematical	`SimpleGraph.extremalNumber` `Fintype.card` `Finset.card` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet` `Sym2.instFintype`	`SimpleGraph.IsContained`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `SimpleGraph.card_edgeFinset_le_extremalNumber`

SimpleGraph.IsExtremal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_iff_eq` 📖	mathematical	`SimpleGraph.IsExtremal`	`SimpleGraph` `SimpleGraph.instLE`	—	`Finset.eq_of_subset_of_card_le` `SimpleGraph.edgeFinset_subset_edgeFinset` `le_of_eq`
`prop` 📖	—	`SimpleGraph.IsExtremal`	—	—	—

---

← Back to Index