Structures · Combinatorics
SimpleGraph.TripartiteFromTriangles.NoAccidental
Predicate on the triangle indices for there to be no accidental triangle.
Note that we cheat a bit, since the exact translation of this informal description would have
(a', b', c') ∈ t as a conclusion rather than a = a' ∨ b = b' ∨ c = c'. Those conditions are
equivalent when the explicit triangles are edge-disjoint (which is the case we care about).
- Shape
- One type argument · adds eq_or_eq_or_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image
- SimpleGraph.TripartiteFromTriangles.is3Clique_iff
- SimpleGraph.TripartiteFromTriangles.card_triangles
- SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image
- SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map
- SimpleGraph.TripartiteFromTriangles.NoAccidental.eq_or_eq_or_eq
- SimpleGraph.TripartiteFromTriangles.locallyLinear
- SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn
Ancestors0
No ancestors.