in₂₀_iff — Mathlib

English

There is an edge between in2 c and in0 a iff there exists b with (a,b,c) ∈ t.

Русский

Существует ребро между in2 c и in0 a ⇔ найдётся b, такое что (a,b,c) ∈ t.

LaTeX

$$$(graph\\ t).Adj(\\mathrm{in}_2 c)(\\mathrm{in}_0 a) \\iff \\exists b, (a,b,c) \\in t.$$$

Lean4

@[simp]
theorem in₂₀_iff : (graph t).Adj (in₂ c) (in₀ a) ↔ ∃ b, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₂₀ h⟩

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