in₁₂_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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