center_eq_univ_iff_radius_eq_ediam

English

Let α be nonempty. Then G.center = Set.univ if and only if G.radius = G.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_iff_radius_eq_ediam [Nonempty α] : G.center = Set.univ ↔ G.radius = G.ediam :=
  by
  rw [radius_eq_ediam_iff, ← Set.univ_subset_iff]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · use G.radius
    exact fun _ ↦ h trivial
  · obtain ⟨e, h⟩ := h
    intro u hu
    rw [mem_center_iff, h u]
    exact le_antisymm (le_iInf fun u ↦ (h u).ge) ((h Classical.ofNonempty) ▸ radius_le_eccent)

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