Documentation Verification Report

Tripartite

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

Statistics

Metric	Count
Definitions `ExplicitDisjoint`, `NoAccidental`, `graph`, `instDecidableRelAdj`, `toTriangle`	5
Theorems `inj₀`, `inj₁`, `inj₂`, `in₀₁_iff`, `in₀₁_iff'`, `in₀₂_iff`, `in₀₂_iff'`, `in₁₀_iff`, `in₁₀_iff'`, `in₁₂_iff`, `in₁₂_iff'`, `in₂₀_iff`, `in₂₀_iff'`, `in₂₁_iff`, `in₂₁_iff'`, `not_in₀₀`, `not_in₁₁`, `not_in₂₂`, `eq_or_eq_or_eq`, `card_triangles`, `cliqueFinset_eq_image`, `cliqueFinset_eq_map`, `cliqueSet_eq_image`, `exists_mem_toTriangle`, `farFromTriangleFree`, `graph_triple`, `is3Clique_iff`, `locallyLinear`, `map_toTriangle_disjoint`, `rel_iff`, `rel_irrefl`, `rel_symm`, `toTriangle_apply`, `toTriangle_is3Clique`, `toTriangle_surjOn`	35
Total	40

SimpleGraph.TripartiteFromTriangles

Definitions

Name	Category	Theorems
`ExplicitDisjoint` 📖	CompData	—
`NoAccidental` 📖	CompData	—
`graph` 📖	CompOp	24 math math: `Graph.in₀₂_iff'`, `toTriangle_surjOn`, `Graph.in₀₁_iff'`, `cliqueFinset_eq_map`, `Graph.in₂₁_iff'`, `Graph.in₁₀_iff`, `is3Clique_iff`, `Graph.in₀₂_iff`, `locallyLinear`, `cliqueSet_eq_image`, `cliqueFinset_eq_image`, `toTriangle_is3Clique`, `Graph.in₁₂_iff'`, `Graph.in₂₀_iff'`, `Graph.not_in₂₂`, `Graph.in₀₁_iff`, `card_triangles`, `Graph.in₂₀_iff`, `Graph.in₁₀_iff'`, `Graph.in₁₂_iff`, `farFromTriangleFree`, `Graph.not_in₀₀`, `Graph.not_in₁₁`, `Graph.in₂₁_iff`
`toTriangle` 📖	CompOp	9 math math: `toTriangle_surjOn`, `cliqueFinset_eq_map`, `is3Clique_iff`, `cliqueSet_eq_image`, `cliqueFinset_eq_image`, `toTriangle_is3Clique`, `exists_mem_toTriangle`, `toTriangle_apply`, `map_toTriangle_disjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_triangles` 📖	mathematical	—	`Finset.card` `Finset` `SimpleGraph.cliqueFinset` `graph` `instFintypeSum` `graph.instDecidableRelAdj`	—	`cliqueFinset_eq_map` `Finset.card_map`
`cliqueFinset_eq_image` 📖	mathematical	—	`SimpleGraph.cliqueFinset` `graph` `instFintypeSum` `graph.instDecidableRelAdj` `Finset.image` `Finset` `Finset.decidableEq` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toTriangle`	—	`Finset.coe_injective` `SimpleGraph.coe_cliqueFinset` `Finset.coe_image` `cliqueSet_eq_image`
`cliqueFinset_eq_map` 📖	mathematical	—	`SimpleGraph.cliqueFinset` `graph` `instFintypeSum` `graph.instDecidableRelAdj` `Finset.map` `Finset` `toTriangle`	—	`cliqueFinset_eq_image` `Finset.map_eq_image`
`cliqueSet_eq_image` 📖	mathematical	—	`SimpleGraph.cliqueSet` `graph` `Set.image` `Finset` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toTriangle` `SetLike.coe` `Finset.instSetLike`	—	`Set.ext` `is3Clique_iff`
`exists_mem_toTriangle` 📖	mathematical	`SimpleGraph.Adj` `graph`	`Finset` `Finset.instMembership` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toTriangle`	—	—
`farFromTriangleFree` 📖	mathematical	`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`	`SimpleGraph.FarFromTriangleFree` `graph` `instFintypeSum` `graph.instDecidableRelAdj`	—	`SimpleGraph.farFromTriangleFree_of_disjoint_triangles` `Function.Injective.injOn` `Function.Embedding.injective` `Finset.map_subset_iff_subset_preimage` `toTriangle_is3Clique` `map_toTriangle_disjoint` `Fintype.card_sum` `Nat.cast_pow` `Nat.cast_add` `Finset.card_map` `add_assoc`
`graph_triple` 📖	mathematical	`SimpleGraph.Adj` `graph`	`Finset` `Finset.instInsert` `Sum3.in₀` `Sum3.in₁` `Finset.instSingleton` `Sum3.in₂`	—	`Finset.ext`
`is3Clique_iff` 📖	mathematical	—	`SimpleGraph.IsNClique` `graph` `Finset` `Finset.instMembership` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toTriangle`	—	`SimpleGraph.is3Clique_iff` `graph_triple` `Graph.in₀₁_iff` `Graph.in₀₂_iff` `Graph.in₁₂_iff` `NoAccidental.eq_or_eq_or_eq` `toTriangle_is3Clique`
`locallyLinear` 📖	mathematical	—	`SimpleGraph.LocallyLinear` `graph`	—	`cliqueSet_eq_image` `Finset.coe_map` `map_toTriangle_disjoint` `exists_mem_toTriangle` `toTriangle_is3Clique`
`map_toTriangle_disjoint` 📖	mathematical	—	`Set.Pairwise` `Finset` `SetLike.coe` `Finset.instSetLike` `Finset.map` `toTriangle` `Set.Subsingleton` `Set` `Set.instInter`	—	`Finset.coe_map` `ExplicitDisjoint.inj₂` `ExplicitDisjoint.inj₁` `ExplicitDisjoint.inj₀`
`rel_iff` 📖	mathematical	—	`Rel` `Finset` `Finset.instMembership` `Sum3.in₀` `Sum3.in₁` `Sum3.in₂`	—	—
`rel_irrefl` 📖	mathematical	—	`Rel`	—	—
`rel_symm` 📖	mathematical	—	`Symmetric` `Rel`	—	—
`toTriangle_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Finset` `Function.instFunLikeEmbedding` `toTriangle` `Finset.instInsert` `Sum3.in₀` `Sum3.in₁` `Finset.instSingleton` `Sum3.in₂`	—	—
`toTriangle_is3Clique` 📖	mathematical	`Finset` `Finset.instMembership`	`SimpleGraph.IsNClique` `graph` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toTriangle`	—	—
`toTriangle_surjOn` 📖	mathematical	—	`Set.SurjOn` `Finset` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toTriangle` `SetLike.coe` `Finset.instSetLike` `SimpleGraph.cliqueSet` `graph`	—	`is3Clique_iff`

SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inj₀` 📖	—	`Finset` `Finset.instMembership`	—	—	—
`inj₁` 📖	—	`Finset` `Finset.instMembership`	—	—	—
`inj₂` 📖	—	`Finset` `Finset.instMembership`	—	—	—

SimpleGraph.TripartiteFromTriangles.Graph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`in₀₁_iff` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₀` `Sum3.in₁` `Finset` `Finset.instMembership`	—	—
`in₀₁_iff'` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₀` `Sum3.in₁` `Finset` `Finset.instMembership`	—	—
`in₀₂_iff` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₀` `Sum3.in₂` `Finset` `Finset.instMembership`	—	—
`in₀₂_iff'` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₀` `Sum3.in₂` `Finset` `Finset.instMembership`	—	—
`in₁₀_iff` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₁` `Sum3.in₀` `Finset` `Finset.instMembership`	—	—
`in₁₀_iff'` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₁` `Sum3.in₀` `Finset` `Finset.instMembership`	—	—
`in₁₂_iff` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₁` `Sum3.in₂` `Finset` `Finset.instMembership`	—	—
`in₁₂_iff'` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₁` `Sum3.in₂` `Finset` `Finset.instMembership`	—	—
`in₂₀_iff` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₂` `Sum3.in₀` `Finset` `Finset.instMembership`	—	—
`in₂₀_iff'` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₂` `Sum3.in₀` `Finset` `Finset.instMembership`	—	—
`in₂₁_iff` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₂` `Sum3.in₁` `Finset` `Finset.instMembership`	—	—
`in₂₁_iff'` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₂` `Sum3.in₁` `Finset` `Finset.instMembership`	—	—
`not_in₀₀` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₀`	—	—
`not_in₁₁` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₁`	—	—
`not_in₂₂` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.TripartiteFromTriangles.graph` `Sum3.in₂`	—	—

SimpleGraph.TripartiteFromTriangles.NoAccidental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_eq_or_eq` 📖	—	`Finset` `Finset.instMembership`	—	—	—

SimpleGraph.TripartiteFromTriangles.graph

Definitions

Name	Category	Theorems
`instDecidableRelAdj` 📖	CompOp	4 math math: `SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map`, `SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image`, `SimpleGraph.TripartiteFromTriangles.card_triangles`, `SimpleGraph.TripartiteFromTriangles.farFromTriangleFree`

---

← Back to Index