mem_support — Mathlib

English

For a subgraph H of G and a vertex v, v belongs to the support of H exactly when there exists a vertex w with H.Adj(v,w).

Русский

Для подграфа H графа G и вершины v верно: v принадлежит опоре H тогда и только тогда, когда существует вершина w такая, что H.Adj(v,w).

LaTeX

$$$v \\in H.support \\iff \\exists w,\; H.Adj(v,w)$$$

Lean4

theorem mem_support (H : Subgraph G) {v : V} : v ∈ H.support ↔ ∃ w, H.Adj v w :=
  Iff.rfl

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