exists_mem_toTriangle — Mathlib

English

If two vertices x and y are adjacent in the tripartite graph built from t, there exists a triangle z in t such that x and y both lie in the triangle corresponding to z.

Русский

Если две вершины x и y соседствуют в графе, образованном из t, существует треугольник z в t, такой что x и y принадлежат треугольнику, соответствующему z.

LaTeX

$$$\forall x,y:\alpha\oplus\beta\oplus\gamma,\ (graph\ t).Adj\ x\ y\ \Rightarrow\ \exists z\in t:\ x\in toTriangle\ z \wedge y\in toTriangle\ z$$$

Lean4

theorem exists_mem_toTriangle {x y : α ⊕ β ⊕ γ} (hxy : (graph t).Adj x y) :
    ∃ z ∈ t, x ∈ toTriangle z ∧ y ∈ toTriangle z := by cases hxy <;> exact ⟨_, ‹_›, by simp⟩

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