Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-01 17:02 a3c753c4

View on Github →

feat(topology/[subset_properties, separation]): bornologies for filter.co[closed_]compact (#12927)

Estimated changes

Modified src/topology/separation.lean

added theorem bornology.relatively_compact.is_bounded_iff

added def bornology.relatively_compact

added theorem bornology.relatively_compact_eq_in_compact

added theorem filter.coclosed_compact_le_cofinite

Modified src/topology/subset_properties.lean

added theorem bornology.in_compact.is_bounded_iff

added def bornology.in_compact

added theorem is_compact.compl_mem_coclosed_compact_of_is_closed