toTriangle_surjOn — Mathlib

English

The set of all 3-cliques of graph t is exactly the image of t under the mapping toTriangle; i.e., every 3-clique arises from some z ∈ t.

Русский

Множество всех 3- кликов графа t совпадает с изображением t под отображением toTriangle; каждый 3-клик получен из некоторого z ∈ t.

LaTeX

$$$ (t:Set\ (α\timesβ\timesγ)).SurjOn\ toTriangle\ ((graph\ t).cliqueSet\ 3)$$$

Lean4

theorem toTriangle_surjOn [NoAccidental t] : (t : Set (α × β × γ)).SurjOn toTriangle ((graph t).cliqueSet 3) := fun _ ↦
  is3Clique_iff.1

Похожие утверждения