Theorems · Definition · combinatorics

SimpleGraph.TripartiteFromTriangles.Rel.recOn

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  {motive : (a a_1 : α ⊕ β ⊕ γ) → SimpleGraph.TripartiteFromTriangles.Rel t a a_1 → Prop} {a a_1 : α ⊕ β ⊕ γ}
  (t_1 : SimpleGraph.TripartiteFromTriangles.Rel t a a_1),
  (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₀ a) (Sum3.in₁ b) ⋯) →
    (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₁ b) (Sum3.in₀ a) ⋯) →
      (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₀ a) (Sum3.in₂ c) ⋯) →
        (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₂ c) (Sum3.in₀ a) ⋯) →
          (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₁ b) (Sum3.in₂ c) ⋯) →
            (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₂ c) (Sum3.in₁ b) ⋯) → motive a a_1 t_1

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

0 results in Mathlib

Foundations

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