Commit 2025-08-24 20:06 b5ece632

feat(Topology/MetricSpace/Bounded): add some results (#26766) We add two pairs of results:

lemma isBounded_of_abs_le (C : α) : Bornology.IsBounded {x : α | |x| ≤ C} := ...
lemma isBounded_of_abs_lt (C : α) : Bornology.IsBounded {x : α | |x| < C} := ...

(under suitable assumptions on α) and a version of the Extreme Value Theorem that I found convenient:

theorem exists_forall_le_of_isBounded {f : β → α} (hf : Continuous f) (x₀ : β)
    (h : Bornology.IsBounded {x : β | f x ≤ f x₀}) :
    ∃ x, ∀ y, f x ≤ f y := ...
theorem exists_forall_ge_of_isBounded {f : β → α} (hf : Continuous f) (x₀ : β)
    (h : Bornology.IsBounded {x : β | f x₀ ≤ f x}) :
    ∃ x, ∀ y, f y ≤ f x := ...

(under suitable assumptions on α and β). For an application, see GelfandMazur.lean in Heights.