center_bot — Mathlib

English

The center of the bottom graph on any α equals Set.univ.

Русский

Центр графа без рёбер равен всему множеству вершин.

LaTeX

$$$$ (\perp : \mathrm{SimpleGraph}(\alpha)).\mathrm{center} = \mathrm{Set.univ}. $$$$

Lean4

theorem center_bot : (⊥ : SimpleGraph α).center = Set.univ :=
  by
  cases subsingleton_or_nontrivial α
  · exact center_eq_univ_of_subsingleton
  · rw [Set.eq_univ_iff_forall]
    intro u
    rw [mem_center_iff, eccent_bot, radius_bot]

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