Theorems · Inductive type · combinatorics

SimpleGraph.TripartiteFromTriangles.NoAccidental

{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → Finset (α × β × γ) → Prop

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).

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

10 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms