Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.NoAccidental.eq_or_eq_or_eq

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  [self : SimpleGraph.TripartiteFromTriangles.NoAccidental t] ⦃a a' : α⦄ ⦃b b' : β⦄ ⦃c c' : γ⦄,
  (a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c'

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

1 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SimpleGraph.TripartiteFromTriangles.NoAccidental