Commit 2026-01-21 19:37 b7e3a5d7

View on Github →

feat(HereditarilyLindelof): review and expand API (#33897)

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Support.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

added theorem HereditarilyLindelofSpace.isLindelof

added theorem HereditarilyLindelofSpace.of_forall_isOpen

deleted theorem HereditarilyLindelof_LindelofSets

modified theorem IsLindelof.of_coe

added theorem eq_closed_inter_countable

added theorem eq_closed_inter_nat

modified theorem eq_open_union_countable

added theorem eq_open_union_nat

deleted theorem isLindelof_iff_LindelofSpace

added theorem isLindelof_iff_lindelofSpace