minDegree_pos_of_nontrivial — Mathlib

English

In a nontrivial finite graph G that is preconnected, the minimum degree is positive.

Русский

В ненулевом перестановочном графе G, являющемся предсвязанным, минимальная степень положительна.

LaTeX

$$$[\text{Nontrivial}(V)] [\mathrm{Fintype}(V)] {G} [\mathrm{DecidableRel}(G.Adj)] (h : G.Preconnected) : 0 < G.minDegree$$$

Lean4

theorem minDegree_pos_of_nontrivial [Nontrivial V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj]
    (h : G.Preconnected) : 0 < G.minDegree :=
  by
  obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
  rw [hv]
  exact h.degree_pos_of_nontrivial v

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