in₁₀_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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