support_eq_univ — Mathlib

English

Let G be a nontrivial preconnected graph. Then G.support = Set.univ.

Русский

Пусть G — ненулевой предсвязанный граф. Тогда поддержка графа G равна всему множеству вершин.

LaTeX

$$$[\text{Nontrivial}(V)] \{G : \mathrm{SimpleGraph}(V)\} (h : G.Preconnected) : G.support = \mathrm{Set.univ}$$$

Lean4

theorem support_eq_univ [Nontrivial V] {G : SimpleGraph V} (h : G.Preconnected) : G.support = Set.univ :=
  by
  simp only [Set.eq_univ_iff_forall]
  intro v
  obtain ⟨w, hw⟩ := exists_ne v
  obtain ⟨p⟩ := h v w
  cases p with
  | nil => contradiction
  | @cons _ w => exact ⟨w, ‹_›⟩

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