Theorem Metric.isBounded_of_abs_lt

Modification history

2026-10-13 14:51
Mathlib/Topology/MetricSpace/Bounded.lean
refactor(Data): make `Set` a one-field structure (#41506) …
Modified Metric.isBounded_of_abs_ltView on Github →
2025-08-24 20:06
Mathlib/Topology/MetricSpace/Bounded.lean
feat(Topology/MetricSpace/Bounded): add some results (#26766) …
Added Metric.isBounded_of_abs_ltView on Github →