in₂₁_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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