Theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top

Modification history

2025-09-08 07:33
Mathlib/Topology/LocalAtTarget.lean
chore: remove >6 month deprecations (#29276) …
Deleted isLocallyClosed_iff_coe_preimage_of_iSup_eq_topView on Github →
2024-07-30 18:20
Mathlib/Topology/LocalAtTarget.lean
chore(Topology/LocallyClosed): move around (#15323) …
Modified isLocallyClosed_iff_coe_preimage_of_iSup_eq_topView on Github →
2024-07-24 08:31
Mathlib/Topology/LocallyClosed.lean
chore(Topology/LocallyClosed): use `X`/`Y` instead of `α`/`β` (#15084)
Modified isLocallyClosed_iff_coe_preimage_of_iSup_eq_topView on Github →
2024-07-14 15:55
Mathlib/Topology/LocallyClosed.lean
feat(Topology/LocallyClosed): Define locally closed sets (#14396)
Added isLocallyClosed_iff_coe_preimage_of_iSup_eq_topView on Github →