mem_supp_iff — Mathlib

English

For any connected component C and vertex v, v belongs to C.supp iff G.connectedComponentMk v = C.

Русский

Для любой компоненты C и вершины v верна эквивалентность: v ∈ C.supp тогда и только тогда, когда G.connectedComponentMk v = C.

LaTeX

$$$v \\in C.supp \\iff G.connectedComponentMk v = C$$$

Lean4

@[simp]
theorem mem_supp_iff (C : G.ConnectedComponent) (v : V) : v ∈ C.supp ↔ G.connectedComponentMk v = C :=
  Iff.rfl

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