Theorems · Definition · combinatorics

SimpleGraph.TripartiteFromTriangles.toTriangle

{α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → [DecidableEq α] → [DecidableEq β] → [DecidableEq γ] → α × β × γ ↪ Finset (α ⊕ β ⊕ γ)

The map that turns a triangle index into an explicit triangle.

Defined in

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Cited by

12 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqDecidableEq