fromEdgeSet_adj — Mathlib

English

For any set s, an edge {v,w} is adjacent in fromEdgeSet s exactly when {v,w} ∈ s and v ≠ w.

Русский

Для любого множества s ребро {v,w} смежно в fromEdgeSet s тогда и только тогда, когда {v,w} ∈ s и v ≠ w.

LaTeX

$$$(\\mathrm{fromEdgeSet}(s)).\\mathrm{Adj}(v,w) \\iff (\\{v,w\\} \\in s) \\wedge v \\neq w$$$

Lean4

@[simp]
theorem fromEdgeSet_adj : (fromEdgeSet s).Adj v w ↔ s(v, w) ∈ s ∧ v ≠ w :=
  Iff.rfl

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