Theorem Continuous.exists_forall_le_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_le_of_isBoundedView on Github →