Documentation Verification Report

Turan

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

Statistics

Metric	Count
Definitions `IsTuranMaximal`, `finpartition`, `instDecidableRelR`, `setoid`, `instDecidableRelFinAdjTuranGraph`, `turanGraph`	6
Theorems `card_edgeFinset_le`, `card_parts`, `card_parts_le`, `degree_eq_card_sub_part_card`, `degree_eq_of_not_adj`, `equivalence_not_adj`, `isEquipartition`, `iso`, `nonempty_iso_turanGraph`, `not_adj_iff_part_eq`, `not_adj_trans`, `card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph`, `card_edgeFinset_turanGraph`, `card_edgeFinset_turanGraph_add`, `exists_isTuranMaximal`, `extremalNumber_top`, `isExtremal_top_free_iff_isTuranMaximal`, `isExtremal_top_free_turanGraph`, `isTuranMaximal_iff_nonempty_iso_turanGraph`, `isTuranMaximal_of_iso`, `isTuranMaximal_turanGraph`, `mul_card_edgeFinset_turanGraph_le`, `not_cliqueFree_of_isTuranMaximal`, `turanGraph_adj`, `turanGraph_cliqueFree`, `turanGraph_eq_top`, `turanGraph_zero`	27
Total	33

SimpleGraph

Definitions

Name	Category	Theorems
`IsTuranMaximal` 📖	MathDef	5 math math: `isExtremal_top_free_iff_isTuranMaximal`, `isTuranMaximal_turanGraph`, `exists_isTuranMaximal`, `isTuranMaximal_iff_nonempty_iso_turanGraph`, `isTuranMaximal_of_iso`
`instDecidableRelFinAdjTuranGraph` 📖	CompOp	6 math math: `isTuranMaximal_turanGraph`, `card_edgeFinset_turanGraph_add`, `extremalNumber_top`, `isExtremal_top_free_turanGraph`, `card_edgeFinset_turanGraph`, `mul_card_edgeFinset_turanGraph_le`
`turanGraph` 📖	CompOp	13 math math: `turanGraph_eq_top`, `isTuranMaximal_turanGraph`, `turanGraph_cliqueFree`, `IsTuranMaximal.nonempty_iso_turanGraph`, `card_edgeFinset_turanGraph_add`, `extremalNumber_top`, `isExtremal_top_free_turanGraph`, `turanGraph_zero`, `turanGraph_adj`, `isTuranMaximal_iff_nonempty_iso_turanGraph`, `card_edgeFinset_turanGraph`, `card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph`, `mul_card_edgeFinset_turanGraph_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph` 📖	mathematical	—	`Free` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `extremalNumber` `Fintype.card` `Iso` `turanGraph`	—	`isTuranMaximal_iff_nonempty_iso_turanGraph` `Fintype.one_lt_card` `isExtremal_top_free_iff_isTuranMaximal` `isExtremal_free_iff`
`card_edgeFinset_turanGraph` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `turanGraph` `fintypeEdgeSet` `Sym2.instFintype` `Fin.fintype` `instDecidableRelFinAdjTuranGraph` `Monoid.toNatPow` `Nat.instMonoid` `Nat.choose`	—	—
`card_edgeFinset_turanGraph_add` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `turanGraph` `fintypeEdgeSet` `Sym2.instFintype` `Fin.fintype` `instDecidableRelFinAdjTuranGraph` `Nat.choose`	—	`mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `two_ne_zero` `mul_add` `Distrib.leftDistribClass` `Finset.sum_congr` `neighborFinset_eq_filter` `Finset.card_filter` `Fin.sum_univ_eq_sum_range` `Finset.sum_range_add` `Finset.sum_add_distrib` `add_assoc` `Finset.sum_comm` `Nat.instAtLeastTwoHAddOfNat` `Finset.card_range` `smul_eq_mul` `Finset.sum_const` `mul_comm` `Nat.choose_two_right` `Nat.div_two_mul_two_of_even` `Nat.even_mul_pred_self`
`exists_isTuranMaximal` 📖	mathematical	—	`IsTuranMaximal`	—	`cliqueFree_bot`
`extremalNumber_top` 📖	mathematical	—	`extremalNumber` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Finset.card` `Sym2` `edgeFinset` `turanGraph` `Fintype.card` `fintypeEdgeSet` `Sym2.instFintype` `Fin.fintype` `instDecidableRelFinAdjTuranGraph`	—	`Fintype.card_fin` `card_edgeFinset_of_isExtremal_free` `isExtremal_top_free_turanGraph`
`isExtremal_top_free_iff_isTuranMaximal` 📖	mathematical	—	`IsExtremal` `Free` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `IsTuranMaximal` `Fintype.card`	—	`Fintype.card_ne_zero` `Nontrivial.to_nonempty`
`isExtremal_top_free_turanGraph` 📖	mathematical	—	`IsExtremal` `Fin.fintype` `turanGraph` `Fintype.card` `instDecidableRelFinAdjTuranGraph` `Free` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`isExtremal_top_free_iff_isTuranMaximal` `isTuranMaximal_turanGraph` `Fintype.one_lt_card`
`isTuranMaximal_iff_nonempty_iso_turanGraph` 📖	mathematical	—	`IsTuranMaximal` `Iso` `Fintype.card` `turanGraph`	—	`IsTuranMaximal.nonempty_iso_turanGraph` `isTuranMaximal_of_iso`
`isTuranMaximal_of_iso` 📖	mathematical	—	`IsTuranMaximal`	—	`exists_isTuranMaximal` `IsTuranMaximal.nonempty_iso_turanGraph` `CliqueFree.comap` `turanGraph_cliqueFree` `Iso.card_edgeFinset_eq` `Fintype.card_fin` `Iso.card_eq`
`isTuranMaximal_turanGraph` 📖	mathematical	—	`IsTuranMaximal` `Fin.fintype` `turanGraph` `instDecidableRelFinAdjTuranGraph`	—	`isTuranMaximal_of_iso`
`mul_card_edgeFinset_turanGraph_le` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `turanGraph` `fintypeEdgeSet` `Sym2.instFintype` `Fin.fintype` `instDecidableRelFinAdjTuranGraph` `Monoid.toNatPow` `Nat.instMonoid`	—	`card_edgeFinset_turanGraph` `mul_add` `Distrib.leftDistribClass` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_refl` `tsub_mul` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `mul_le_mul_left` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `mul_comm` `Nat.choose_two_right` `Nat.instAtLeastTwoHAddOfNat` `Even.two_dvd` `Nat.even_mul_pred_self` `mul_assoc` `mul_div_cancel_left₀` `Nat.instMulDivCancelClass` `two_ne_zero` `mul_rotate` `sq` `LT.lt.le`
`not_cliqueFree_of_isTuranMaximal` 📖	mathematical	`Fintype.card` `IsTuranMaximal`	`CliqueFree`	—	`Finset.exists_subset_card_eq` `LE.le.trans_eq` `le_sup_right` `IsExtremal.le_iff_eq` `CliqueFree.sup_edge` `le_sup_left` `edge_adj`
`turanGraph_adj` 📖	mathematical	—	`Adj` `turanGraph`	—	—
`turanGraph_cliqueFree` 📖	mathematical	—	`CliqueFree` `turanGraph`	—	`cliqueFree_iff` `Fintype.exists_ne_map_eq_of_card_lt` `Fintype.card_fin` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`
`turanGraph_eq_top` 📖	mathematical	—	`turanGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `LT.lt.trans` `LT.lt.trans_le`
`turanGraph_zero` 📖	mathematical	—	`turanGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—

SimpleGraph.CliqueFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_edgeFinset_le` 📖	mathematical	`SimpleGraph.CliqueFree`	`Finset.card` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet` `Sym2.instFintype` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Nat.choose`	—	`zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `MulZeroClass.mul_zero` `zero_add` `SimpleGraph.card_edgeFinset_le_card_choose_two` `SimpleGraph.exists_isTuranMaximal` `SimpleGraph.Iso.card_edgeFinset_eq` `SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph` `SimpleGraph.card_edgeFinset_turanGraph`

SimpleGraph.IsTuranMaximal

Definitions

Name	Category	Theorems
`finpartition` 📖	CompOp	5 math math: `not_adj_iff_part_eq`, `card_parts_le`, `isEquipartition`, `card_parts`, `degree_eq_card_sub_part_card`
`instDecidableRelR` 📖	CompOp	—
`setoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_parts` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `finpartition` `Fintype.card`	—	`le_antisymm` `le_min` `Finpartition.card_parts_le_card` `card_parts_le` `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` `lt_min_iff` `Finpartition.part_mem` `Finset.mem_univ` `eq_1` `SimpleGraph.IsExtremal.eq_1` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `not_adj_iff_part_eq` `SimpleGraph.CliqueFree.sup_edge` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `SimpleGraph.card_edgeFinset_sup_edge`
`card_parts_le` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `finpartition`	—	`Finpartition.exists_subset_part_bijOn` `SimpleGraph.IsNClique.not_cliqueFree` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.BijOn.injOn` `not_adj_iff_part_eq` `SimpleGraph.CliqueFree.mono` `Finset.card_eq_of_equiv`
`degree_eq_card_sub_part_card` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`SimpleGraph.degree` `SimpleGraph.neighborSetFintype` `Fintype.card` `Finset.card` `Finpartition.part` `Finset.univ` `finpartition`	—	`Set.toFinset_card` `Fintype.card_ofFinset` `Finset.filter.congr_simp` `eq_tsub_of_add_eq` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.card_filter_add_card_filter_not` `Finset.ext` `Finset.mem_filter` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `Finpartition.mem_part_ofSetoid_iff_rel`
`degree_eq_of_not_adj` 📖	mathematical	`SimpleGraph.IsTuranMaximal` `SimpleGraph.Adj`	`SimpleGraph.degree` `SimpleGraph.neighborSetFintype`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `SimpleGraph.CliqueFree.replaceVertex` `SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj` `lt_of_le_of_ne` `le_of_not_gt` `SimpleGraph.adj_comm` `LT.lt.ne'` `SimpleGraph.IsExtremal.eq_1` `eq_1`
`equivalence_not_adj` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`SimpleGraph.Adj`	—	`not_adj_trans`
`isEquipartition` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`Finpartition.IsEquipartition` `Finset.univ` `finpartition`	—	`Finpartition.not_isEquipartition` `Finpartition.nonempty_of_mem_parts` `eq_1` `SimpleGraph.IsExtremal.eq_1` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `SimpleGraph.CliqueFree.replaceVertex` `Finpartition.part_eq_of_mem` `not_adj_iff_part_eq` `SimpleGraph.card_edgeFinset_replaceVertex_of_adj` `degree_eq_card_sub_part_card` `Finset.card_le_card` `Finset.subset_univ`
`iso` 📖	—	`SimpleGraph.IsTuranMaximal`	—	—	`SimpleGraph.isTuranMaximal_of_iso` `nonempty_iso_turanGraph`
`nonempty_iso_turanGraph` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`SimpleGraph.Iso` `Fintype.card` `SimpleGraph.turanGraph`	—	`Finpartition.IsEquipartition.exists_partPreservingEquiv` `isEquipartition` `Finset.mem_univ` `not_iff_not` `not_ne_iff` `not_adj_iff_part_eq` `card_parts` `le_or_gt` `min_eq_right` `min_eq_left` `LT.lt.le` `LT.lt.trans`
`not_adj_iff_part_eq` 📖	mathematical	`SimpleGraph.IsTuranMaximal`	`SimpleGraph.Adj` `Finpartition.part` `Finset.univ` `finpartition`	—	`Finpartition.mem_part_ofSetoid_iff_rel` `Finpartition.mem_part_iff_part_eq_part` `Finset.mem_univ`
`not_adj_trans` 📖	—	`SimpleGraph.IsTuranMaximal` `SimpleGraph.Adj`	—	—	`SimpleGraph.Adj.symm` `degree_eq_of_not_adj` `Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `SimpleGraph.CliqueFree.replaceVertex` `SimpleGraph.ne_of_adj` `Iff.not` `SimpleGraph.adj_replaceVertex_iff_of_ne` `SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj` `Finset.ext` `SimpleGraph.degree.eq_1` `Finset.card_singleton` `Finset.card_sdiff_of_subset` `SimpleGraph.degree_pos_iff_exists_adj` `SimpleGraph.IsExtremal.eq_1` `eq_1`

---

← Back to Index