in₀₁_iff' — Mathlib

English

A variant form of the α-β edge criterion: there exists a triple in t whose coordinates match a and b in the first two coordinates.

Русский

Вариант формулы для ребра α-β: существует элемент t, координаты которого совпадают с a и b в первых двух местах.

LaTeX

$$$(graph\\ t).Adj(\\mathrm{in}_0 a)(\\mathrm{in}_1 b) \\iff \\exists x=(a',b',c'), x\\in t \\land a'=a \\land b'=b.$$$

Lean4

theorem in₀₁_iff' : (graph t).Adj (in₀ a) (in₁ b) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.1 = a ∧ x.2.1 = b
    where
  mp := by rintro ⟨⟩; exact ⟨_, ‹_›, by simp⟩
  mpr := by rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩; constructor; assumption

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