Theorem Real.atTop_le_cocompact

Modification history

2024-02-09 14:17
Mathlib/Topology/Instances/Real.lean
feat: generalize `cocompact_eq` (#10285) …
Deleted Real.atTop_le_cocompactView on Github →
2023-10-30 20:20
Mathlib/Topology/Instances/Real.lean
feat: additional version of FTC-2 for improper integrals (#7755) …
Added Real.atTop_le_cocompactView on Github →