Theorem IsLindelof.countable_of_isDiscrete

Modification history

2025-12-17 17:45
Mathlib/Topology/Compactness/Lindelof.lean
feat: meromorphic functions are measurable (#32675) …
Added IsLindelof.countable_of_isDiscreteView on Github →