center_eq_univ_of_subsingleton — Mathlib

English

Let α be nonempty. Then G.center = Set.univ if and only if radius equals ediam.

Русский

Пусть α непусто. Тогда center(G) = Set.univ ⇔ radius(G) = ediam(G).

LaTeX

$$$$ G.center = \mathrm{Set.univ} \iff G.radius = G.ediam. $$$$

Lean4

theorem center_eq_univ_of_subsingleton [Subsingleton α] : G.center = Set.univ :=
  by
  rw [Set.eq_univ_iff_forall]
  intro u
  rw [mem_center_iff, eccent_eq_zero_of_subsingleton u, eq_comm, radius_eq_zero_iff]
  tauto

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