Theorem Continuous.exists_forall_ge_of_isBounded

Modification history

2025-08-24 20:06
Mathlib/Topology/MetricSpace/Bounded.lean
feat(Topology/MetricSpace/Bounded): add some results (#26766) …
Added Continuous.exists_forall_ge_of_isBoundedView on Github →