English
There exists an order-bornology structure on α if every closed or compact ball has bounded below and above.
Русский
Существует структура IsOrderBornology на α, если для каждого замкнутого шарa существуют границы снизу и сверху.
LaTeX
$$$IsOrderBornology(\\\\alpha)\\,\\text{ holds if } (\\forall r, BddBelow(closedBall(x,r))\\land BddAbove(closedBall(x,r))).$$$
Lean4
theorem _root_.IsOrderBornology.of_isCompactIcc (x : α) (bddBelow_ball : ∀ r, BddBelow (closedBall x r))
(bddAbove_ball : ∀ r, BddAbove (closedBall x r)) : IsOrderBornology α where
isBounded_iff_bddBelow_bddAbove
s := by
refine ⟨?_, fun hs ↦ Metric.isBounded_of_bddAbove_of_bddBelow hs.2 hs.1⟩
rw [Metric.isBounded_iff_subset_closedBall x]
rintro ⟨r, hr⟩
exact ⟨(bddBelow_ball _).mono hr, (bddAbove_ball _).mono hr⟩
