degree_eq_one_iff_unique_adj — Mathlib

English

Degree equals one iff there exists a unique adjacent vertex.

Русский

Степень равна единице тогда и только тогда существует едиственный сосед.

LaTeX

$$$G'.degree v = 1 \iff \exists! w : V, G'.Adj v w$$$

Lean4

theorem degree_eq_one_iff_unique_adj {G' : Subgraph G} {v : V} [Fintype (G'.neighborSet v)] :
    G'.degree v = 1 ↔ ∃! w : V, G'.Adj v w :=
  by
  rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
  simp only [Set.mem_toFinset, mem_neighborSet]

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