Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `EdgeDisjointTriangles`, `instDecidable`, `FarFromTriangleFree`, `LocallyLinear`, `instDecidable`	5
Theorems `not_farFromTriangleFree`, `card_edgeFinset_le`, `farFromTriangleFree`, `map`, `mem_sym2_subsingleton`, `mono`, `cliqueFinset_nonempty`, `cliqueFinset_nonempty'`, `lt_half`, `lt_one`, `mono`, `nonpos`, `not_cliqueFree`, `card_edgeFinset`, `edgeDisjointTriangles`, `map`, `edgeDisjointTriangles_bot`, `edgeDisjointTriangles_iff_mem_sym2_subsingleton`, `le_card_sub_card`, `farFromTriangleFree_iff`, `farFromTriangleFree_of_disjoint_triangles`, `locallyLinear_bot`, `locallyLinear_comap`	23
Total	28

SimpleGraph

Definitions

Name	Category	Theorems
`EdgeDisjointTriangles` 📖	MathDef	3 math math: `LocallyLinear.edgeDisjointTriangles`, `edgeDisjointTriangles_bot`, `edgeDisjointTriangles_iff_mem_sym2_subsingleton`
`FarFromTriangleFree` 📖	MathDef	5 math math: `farFromTriangleFree_iff`, `farFromTriangleFree_of_disjoint_triangles`, `CliqueFree.not_farFromTriangleFree`, `EdgeDisjointTriangles.farFromTriangleFree`, `TripartiteFromTriangles.farFromTriangleFree`
`LocallyLinear` 📖	MathDef	4 math math: `locallyLinear_bot`, `ruzsaSzemerediNumber_spec`, `TripartiteFromTriangles.locallyLinear`, `locallyLinear_comap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edgeDisjointTriangles_bot` 📖	mathematical	—	`EdgeDisjointTriangles` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`cliqueSet_bot` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero`
`edgeDisjointTriangles_iff_mem_sym2_subsingleton` 📖	mathematical	—	`EdgeDisjointTriangles` `Set.Subsingleton` `Finset` `setOf` `Set` `Set.instMembership` `cliqueSet` `Sym2` `Finset.instMembership` `Finset.sym2`	—	`Set.ext` `Finset.ext` `Sym2.forall` `Iff.not` `Sym2.mk_isDiag_iff` `Set.Pairwise.eq` `Set.Nontrivial.not_subsingleton` `Finset.coe_insert` `Finset.coe_singleton` `Adj.ne` `Set.not_nontrivial_iff`
`farFromTriangleFree_iff` 📖	mathematical	—	`FarFromTriangleFree` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`deleteFar_iff`
`farFromTriangleFree_of_disjoint_triangles` 📖	mathematical	`Finset` `Finset.instHasSubset` `cliqueFinset` `Set.Pairwise` `SetLike.coe` `Finset.instSetLike` `Set.Subsingleton` `Set` `Set.instInter` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finset.card`	`FarFromTriangleFree`	—	`farFromTriangleFree_iff` `Nat.cast_sub` `Finset.card_le_card` `edgeFinset_mono` `LE.le.trans` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero`
`locallyLinear_bot` 📖	mathematical	—	`LocallyLinear` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`locallyLinear_comap` 📖	mathematical	—	`LocallyLinear` `comap` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`comap_map_eq` `comap_symm` `map_symm` `LocallyLinear.map` `Equiv.coe_toEmbedding`

SimpleGraph.CliqueFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_farFromTriangleFree` 📖	mathematical	`SimpleGraph.CliqueFree` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`SimpleGraph.FarFromTriangleFree`	—	`LE.le.not_gt` `SimpleGraph.FarFromTriangleFree.nonpos`

SimpleGraph.EdgeDisjointTriangles

Definitions

Name	Category	Theorems
`instDecidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_edgeFinset_le` 📖	mathematical	`SimpleGraph.EdgeDisjointTriangles`	`Finset.card` `Finset` `SimpleGraph.cliqueFinset` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet` `Sym2.instFintype`	—	`mul_comm` `mul_one` `Finset.card_mul_le_card_mul` `Finset.bipartiteAbove.congr_simp` `Finset.card_eq_three` `SimpleGraph.Adj.ne` `Finset.card_mono` `mem_sym2_subsingleton` `SimpleGraph.not_isDiag_of_mem_edgeSet` `SimpleGraph.mem_edgeFinset`
`farFromTriangleFree` 📖	mathematical	`SimpleGraph.EdgeDisjointTriangles` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finset.card` `Finset` `SimpleGraph.cliqueFinset`	`SimpleGraph.FarFromTriangleFree`	—	`SimpleGraph.farFromTriangleFree_of_disjoint_triangles` `Finset.Subset.rfl` `SimpleGraph.coe_cliqueFinset`
`map` 📖	mathematical	`SimpleGraph.EdgeDisjointTriangles`	`SimpleGraph.map`	—	`eq_1` `SimpleGraph.cliqueSet_map` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Set.InjOn.pairwise_image` `Function.Injective.injOn` `Finset.map_injective` `Finset.coe_inter` `Finset.map_inter` `Finset.coe_map` `Set.Subsingleton.image`
`mem_sym2_subsingleton` 📖	mathematical	`SimpleGraph.EdgeDisjointTriangles` `Sym2.IsDiag`	`Set.Subsingleton` `Finset` `setOf` `Set` `Set.instMembership` `SimpleGraph.cliqueSet` `Sym2` `Finset.instMembership` `Finset.sym2`	—	`SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton`
`mono` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.EdgeDisjointTriangles`	—	—	`Set.Pairwise.mono` `SimpleGraph.cliqueSet_mono`

SimpleGraph.FarFromTriangleFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cliqueFinset_nonempty` 📖	mathematical	`SimpleGraph.FarFromTriangleFree` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Finset.Nonempty` `Finset` `SimpleGraph.cliqueFinset`	—	`Finset.nonempty_of_ne_empty` `Iff.not` `SimpleGraph.cliqueFinset_eq_empty_iff` `not_cliqueFree`
`cliqueFinset_nonempty'` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.FarFromTriangleFree` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.card` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet` `Sym2.instFintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card`	`Finset.Nonempty` `Finset` `SimpleGraph.cliqueFinset`	—	`Finset.nonempty_of_ne_empty` `Iff.not` `SimpleGraph.cliqueFinset_eq_empty_iff` `LE.le.not_gt` `SimpleGraph.DeleteFar.le_card_sub_card`
`lt_half` 📖	mathematical	`SimpleGraph.FarFromTriangleFree`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.instAtLeastTwoHAddOfNat`	—	`lt_of_mul_lt_mul_right` `Nat.instAtLeastTwoHAddOfNat` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_pow` `SimpleGraph.DeleteFar.le_card_edgeFinset` `Nat.mono_cast` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `SimpleGraph.card_edgeFinset_le_card_choose_two` `Nat.choose_lt_pow_div` `ne_of_gt` `Fintype.card_pos` `le_rfl` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos'` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`lt_one` 📖	mathematical	`SimpleGraph.FarFromTriangleFree`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`LT.lt.trans` `Nat.instAtLeastTwoHAddOfNat` `lt_half` `two_inv_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`mono` 📖	—	`SimpleGraph.FarFromTriangleFree` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`SimpleGraph.DeleteFar.mono` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass`
`nonpos` 📖	mathematical	`SimpleGraph.FarFromTriangleFree` `SimpleGraph.CliqueFree`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Finset.empty_subset` `nonpos_of_mul_nonpos_left` `IsStrictOrderedRing.toPosMulStrictMono` `SimpleGraph.deleteEdges_empty` `Nat.cast_zero` `Finset.card_empty` `Finset.coe_empty` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `sq_pos_of_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Fintype.card_pos`
`not_cliqueFree` 📖	mathematical	`SimpleGraph.FarFromTriangleFree` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`SimpleGraph.CliqueFree`	—	`LE.le.not_gt` `nonpos`

SimpleGraph.LocallyLinear

Definitions

Name	Category	Theorems
`instDecidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_edgeFinset` 📖	mathematical	`SimpleGraph.LocallyLinear`	`Finset.card` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet` `Sym2.instFintype` `Finset` `SimpleGraph.cliqueFinset`	—	`LE.le.antisymm'` `SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le` `edgeDisjointTriangles` `mul_comm` `mul_one` `Finset.card_mul_le_card_mul` `Finset.bipartiteAbove.congr_simp` `Finset.card_le_card` `Finset.bipartiteBelow.congr_simp` `LE.le.trans` `Finset.card_insert_le` `LE.le.trans_eq` `Finset.card_singleton`
`edgeDisjointTriangles` 📖	mathematical	`SimpleGraph.LocallyLinear`	`SimpleGraph.EdgeDisjointTriangles`	—	—
`map` 📖	mathematical	`SimpleGraph.LocallyLinear`	`SimpleGraph.map`	—	`SimpleGraph.EdgeDisjointTriangles.map` `SimpleGraph.IsNClique.map` `Finset.mem_map_of_mem`

SimpleGraph.farFromTriangleFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_card_sub_card` 📖	mathematical	`SimpleGraph.FarFromTriangleFree` `SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.CliqueFree`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Finset.card` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet` `Sym2.instFintype`	—	`SimpleGraph.farFromTriangleFree_iff`

---

← Back to Index