Commit 2024-01-19 10:45 4a739b98

View on Github →

feat: add Lindelöf spaces and sets (#9107) Add definition Lindelöf set, Lindelöf space, non-Lindelöf space. Add copyright header

Estimated changes

added theorem IsClosed.isLindelof
added theorem IsCompact.isLindelof
added theorem IsLindelof.countable
added theorem IsLindelof.diff
added theorem IsLindelof.image
added theorem IsLindelof.inter_left
added theorem IsLindelof.inter_right
added theorem IsLindelof.ne_univ
added theorem IsLindelof.of_coe
added theorem IsLindelof.union
added def IsLindelof
added theorem Set.Finite.isLindelof
added theorem Subtype.isLindelof_iff
added theorem coLindelof_le_cofinite
added theorem countable_cover_nhds
added theorem hasBasis_coLindelof
added theorem isLindelof_accumulate
added theorem isLindelof_diagonal
added theorem isLindelof_empty
added theorem isLindelof_iUnion
added theorem isLindelof_range
added theorem isLindelof_singleton
added theorem isLindelof_univ
added theorem isLindelof_univ_iff
added theorem mem_coLindelof'
added theorem mem_coLindelof
added theorem mem_coclosedLindelof
added theorem mem_coclosed_Lindelof'
added theorem nonLindelof_univ
added theorem not_LindelofSpace_iff