Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.graph_triple

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] ⦃x y z : α ⊕ β ⊕ γ⦄,
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y →
    (SimpleGraph.TripartiteFromTriangles.graph t).Adj x z →
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj y z →
        ∃ a b c,
          {Sum3.in₀ a, Sum3.in₁ b, Sum3.in₂ c} = {x, y, z} ∧
            (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ∧
              (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ∧
                (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c)

This lemma reorders the elements of a triangle in the tripartite graph. It turns a triangle {x, y, z} into a triangle {a, b, c} where a : α , b : β, c : γ.

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqDecidableEq