Commit 2024-07-30 18:20 ad356e50

View on Github →

chore(Topology/LocallyClosed): move around (#15323)

move definitions to Topology/Defs/Basic;
move the last lemma to Topology/LocalAtTarget.

Estimated changes

Modified Mathlib/Topology/Defs/Basic.lean

added def IsLocallyClosed

added def coborder

Modified Mathlib/Topology/LocalAtTarget.lean

added theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top

Modified Mathlib/Topology/LocallyClosed.lean

deleted def IsLocallyClosed

deleted def coborder

deleted theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top