edge_le_iff — Mathlib

English

For any v,w, edge v w ≤ G holds iff v = w or G.Adj v w.

Русский

Для любых v,w выполняется, что edge(v,w) ≤ G тогда и только тогда, когда v = w или G.Adj v w.

LaTeX

$$$ \text{edge}(v,w) \le G \iff v = w \lor G.Adj(v,w) $$$

Lean4

theorem edge_le_iff {v w : V} : edge v w ≤ G ↔ v = w ∨ G.Adj v w :=
  by
  obtain h | h := eq_or_ne v w
  · simp [h]
  · refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩
    aesop (add simp [edge_adj, adj_symm])

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