Theorems · Theorem · combinatorics

SimpleGraph.TripartiteFromTriangles.toTriangle_apply

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ]
  (x : α × β × γ), SimpleGraph.TripartiteFromTriangles.toTriangle x = {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqDecidableEq