Theorem HereditarilyLindelofSpace.of_forall_isOpen

Modification history

2026-01-21 19:37
Mathlib/Topology/Compactness/Lindelof.lean
feat(HereditarilyLindelof): review and expand API (#33897)
Added HereditarilyLindelofSpace.of_forall_isOpenView on Github →