center_top — Mathlib

English

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

Русский

Центр полного графа на любом α равен всему множеству.

LaTeX

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

Lean4

theorem center_top : (⊤ : 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_top, radius_top]

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