mem_supp_congr_adj — Mathlib

English

If u and w are adjacent, then membership in C.supp is preserved between u and w.

Русский

Если u и w соседние, то принадлежность вершин u и w к C.supp совпадает.

LaTeX

$$$G.Adj v w \\Rightarrow (v \\in c.supp \\iff w \\in c.supp)$$$

Lean4

theorem mem_supp_congr_adj {v w : V} (c : G.ConnectedComponent) (hadj : G.Adj v w) : v ∈ c.supp ↔ w ∈ c.supp :=
  by
  simp only [ConnectedComponent.mem_supp_iff] at *
  constructor <;> intro h <;> simp only [← h] <;> apply connectedComponentMk_eq_of_adj
  · exact hadj.symm
  · exact hadj

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