Documentation Verification Report

FiveWheelLike

📁 Source: Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

Statistics

Metric	Count
Definitions `FiveWheelLikeFree`, `IsFiveWheelLike`	2
Theorems `fiveWheelLikeFree_of_le`, `card_inter`, `card_inter_lt_of_cliqueFree`, `card_left`, `card_right`, `exists_isFiveWheelLike_succ_of_not_adj_le_two`, `fst_notMem`, `fst_notMem_right`, `isNClique_fst_left`, `isNClique_left`, `isNClique_right`, `isNClique_snd_right`, `isPathGraph3Compl`, `minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ`, `notMem_left`, `notMem_right`, `not_colorable_succ`, `snd_notMem`, `snd_notMem_left`, `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree`, `colorable_of_cliqueFree_lt_minDegree`, `exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`, `exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`	23
Total	25

SimpleGraph

Definitions

Name	Category	Theorems
`FiveWheelLikeFree` 📖	MathDef	2 math math: `CliqueFree.fiveWheelLikeFree_of_le`, `exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`
`IsFiveWheelLike` 📖	CompData	2 math math: `exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`, `exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree` 📖	mathematical	`Maximal` `SimpleGraph` `instLE` `CliqueFree`	`Colorable` `IsCompleteMultipartite`	—	`cliqueFree_one` `colorable_zero_iff` `Mathlib.Tactic.Contrapose.contrapose₁` `exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite` `IsFiveWheelLike.not_colorable_succ` `IsCompleteMultipartite.colorable_of_cliqueFree`
`colorable_of_cliqueFree_lt_minDegree` 📖	mathematical	`CliqueFree` `Fintype.card` `minDegree`	`Colorable`	—	`MulZeroClass.mul_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Fintype.card_eq_zero` `zero_add` `minDegree_of_isEmpty` `mul_one` `MulZeroClass.zero_mul` `minDegree.congr_simp` `minDegree_bot_eq_zero` `Finite.exists_le_maximal` `instFinite` `Finite.of_fintype` `Colorable.mono_left` `IsCompleteMultipartite.colorable_of_cliqueFree` `exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite` `IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `mul_assoc` `mul_comm` `LE.le.trans` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Linarith.mul_nonpos` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Mathlib.Tactic.Linarith.natCast_nonneg` `Mathlib.Meta.NormNum.isNat_lt_true` `Int.instCharZero` `LT.lt.not_ge` `LT.lt.trans_le` `minDegree_le_minDegree`
`exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite` 📖	mathematical	`Maximal` `SimpleGraph` `instLE` `CliqueFree` `IsCompleteMultipartite`	`IsFiveWheelLike` `Finset.card` `Finset` `Finset.instInter`	—	`exists_isPathGraph3Compl_of_not_isCompleteMultipartite` `exists_of_maximal_cliqueFree_not_adj` `IsPathGraph3Compl.ne_fst` `IsPathGraph3Compl.not_adj_fst` `IsPathGraph3Compl.ne_snd` `IsPathGraph3Compl.not_adj_snd`
`exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite` 📖	mathematical	`Maximal` `SimpleGraph` `instLE` `CliqueFree` `IsCompleteMultipartite`	`IsFiveWheelLike` `FiveWheelLikeFree`	—	`exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite` `Nat.findGreatest_spec` `LT.lt.le` `IsFiveWheelLike.card_inter_lt_of_cliqueFree` `LT.lt.not_ge` `Nat.le_findGreatest`

SimpleGraph.CliqueFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fiveWheelLikeFree_of_le` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph.FiveWheelLikeFree`	—	`LT.lt.not_ge` `SimpleGraph.IsFiveWheelLike.card_inter_lt_of_cliqueFree`

SimpleGraph.IsFiveWheelLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_inter` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset.card` `Finset` `Finset.instInter`	—	—
`card_inter_lt_of_cliqueFree` 📖	—	`SimpleGraph.IsFiveWheelLike` `SimpleGraph.CliqueFree`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Finset.eq_of_subset_of_card_le` `Finset.inter_subset_left` `card_left` `card_inter` `Finset.inter_subset_right` `card_right` `SimpleGraph.IsNClique.not_cliqueFree` `isNClique_fst_left` `isNClique_snd_right` `snd_notMem_left` `SimpleGraph.IsPathGraph3Compl.adj` `isPathGraph3Compl`
`card_left` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset.card`	—	`SimpleGraph.IsNClique.card_eq` `isNClique_left` `Finset.card_insert_of_notMem` `notMem_left`
`card_right` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset.card`	—	`card_left` `symm`
`exists_isFiveWheelLike_succ_of_not_adj_le_two` 📖	mathematical	`SimpleGraph.IsFiveWheelLike` `SimpleGraph.CliqueFree` `SimpleGraph.Adj` `Finset.card` `Finset.filter` `Finset` `Finset.instUnion` `Finset.instSingleton`	`Finset.instInsert` `Finset.erase`	—	`LE.le.not_gt` `Finset.two_lt_card_iff` `Mathlib.Tactic.Push.not_and_eq` `SimpleGraph.IsNClique.isClique` `isNClique_left` `Finset.mem_insert_self` `Finset.mem_insert_of_mem` `isNClique_fst_left` `isNClique_snd_right` `Finset.two_lt_card` `Finset.filter.congr_simp` `Finset.union_insert` `Finset.mem_filter` `SimpleGraph.adj_comm` `notMem_left` `Finset.insert_subset_insert` `Finset.mem_insert` `fst_notMem` `isNClique_right` `notMem_right` `snd_notMem` `Finset.insert_inter_distrib` `Finset.erase_inter` `Finset.inter_erase` `Finset.erase_eq_of_notMem` `Finset.notMem_mono` `Finset.inter_subset_left` `Finset.inter_subset_right` `Finset.card_insert_of_notMem` `SimpleGraph.irrefl` `card_inter`
`fst_notMem` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset` `Finset.instMembership`	—	—
`fst_notMem_right` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset` `Finset.instMembership`	—	`SimpleGraph.IsPathGraph3Compl.not_adj_fst` `isPathGraph3Compl` `SimpleGraph.IsNClique.isClique` `isNClique_right` `Finset.mem_insert_self` `Finset.mem_insert_of_mem` `SimpleGraph.IsPathGraph3Compl.ne_fst`
`isNClique_fst_left` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`SimpleGraph.IsNClique` `Finset` `Finset.instInsert`	—	—
`isNClique_left` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`SimpleGraph.IsNClique` `Finset` `Finset.instInsert`	—	—
`isNClique_right` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`SimpleGraph.IsNClique` `Finset` `Finset.instInsert`	—	—
`isNClique_snd_right` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`SimpleGraph.IsNClique` `Finset` `Finset.instInsert`	—	—
`isPathGraph3Compl` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`SimpleGraph.IsPathGraph3Compl`	—	—
`minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ` 📖	mathematical	`SimpleGraph.IsFiveWheelLike` `SimpleGraph.CliqueFree` `SimpleGraph.FiveWheelLikeFree`	`SimpleGraph.minDegree` `Fintype.card`	—	`exists_isFiveWheelLike_succ_of_not_adj_le_two` `Finset.filter.congr_simp` `SimpleGraph.IsNClique.exists_not_adj_of_cliqueFree_succ` `isNClique_fst_left` `Finset.card_pos` `Finset.mem_filter` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Finset.compl_filter` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_three` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `add_assoc` `add_comm` `mul_add` `Distrib.leftDistribClass` `card_inter` `Finset.card_eq_sum_ones` `Finset.mul_sum` `Finset.sum_congr` `mul_one` `mul_comm` `add_le_add` `covariant_swap_add_of_covariant_add` `Finset.sum_le_sum` `SimpleGraph.minDegree_le_degree` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `mul_le_mul_right` `tsub_zero` `Nat.instOrderedSub` `compl_compl` `Finset.eq_univ_of_forall` `Finset.card_eq_zero` `instIsEmptyFalse` `Finset.filter_true` `add_zero` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `MulZeroClass.zero_mul` `Finset.compl_univ` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Finset.two_lt_card` `Finset.mem_insert_self` `Finset.union_insert` `SimpleGraph.IsPathGraph3Compl.ne_fst` `isPathGraph3Compl` `SimpleGraph.IsPathGraph3Compl.ne_snd` `SimpleGraph.IsPathGraph3Compl.fst_ne_snd` `add_mul` `Distrib.rightDistribClass` `Finset.card_add_card_compl` `two_mul` `add_le_add_left`
`notMem_left` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset` `Finset.instMembership`	—	—
`notMem_right` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset` `Finset.instMembership`	—	—
`not_colorable_succ` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`SimpleGraph.Colorable`	—	`SimpleGraph.Coloring.surjOn_of_card_le_isClique` `SimpleGraph.IsNClique.isClique` `isNClique_fst_left` `Fintype.card_fin` `SimpleGraph.IsNClique.card_eq` `isNClique_snd_right` `Finset.coe_insert` `SimpleGraph.Coloring.valid` `SimpleGraph.IsPathGraph3Compl.adj` `isPathGraph3Compl` `isNClique_right` `notMem_right` `isNClique_left` `notMem_left`
`snd_notMem` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset` `Finset.instMembership`	—	—
`snd_notMem_left` 📖	mathematical	`SimpleGraph.IsFiveWheelLike`	`Finset` `Finset.instMembership`	—	`fst_notMem_right` `symm`

---

← Back to Index