Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.rel_iff

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) (a a_1 : α ⊕ β ⊕ γ),
  SimpleGraph.TripartiteFromTriangles.Rel t a a_1 ↔
    (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₁ b) ∨
      (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₀ a_2) ∨
        (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₂ c) ∨
          (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₀ a_2) ∨
            (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₂ c) ∨
              ∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₁ b

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

0 results in Mathlib

Foundations

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