Commit 2024-07-14 15:55 23a58a86

View on Github →

feat(Topology/LocallyClosed): Define locally closed sets (#14396)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Basic.lean

deleted theorem IsClosed.frontier_subset

added theorem disjoint_frontier_iff_isOpen

added theorem frontier_subset_iff_isClosed

Modified Mathlib/Topology/Constructions.lean

added theorem isClosed_preimage_val

Created Mathlib/Topology/LocallyClosed.lean

added theorem Continuous.preimage_coborder_subset

added theorem Embedding.isLocallyClosed_iff

added theorem Inducing.isLocallyClosed_iff

added theorem IsClosed.isLocallyClosed

added theorem IsLocallyClosed.image

added theorem IsLocallyClosed.inter

added theorem IsLocallyClosed.isOpen_preimage_val_closure

added theorem IsLocallyClosed.preimage

added def IsLocallyClosed

added theorem IsOpen.isLocallyClosed

added theorem IsOpenMap.coborder_preimage_subset

added theorem OpenEmbedding.coborder_preimage

added theorem closure_inter_coborder

added def coborder

added theorem coborder_eq_compl_frontier_iff

added theorem coborder_eq_union_frontier_compl

added theorem coborder_eq_univ_iff

added theorem coborder_inter_closure

added theorem coborder_preimage

added theorem isClosed_preimage_val_coborder

added theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top

added theorem isLocallyClosed_iff_isOpen_coborder

added theorem isLocallyClosed_tfae

added theorem subset_coborder