Commit 2024-07-24 08:31 8ef25050

View on Github →

chore(Topology/LocallyClosed): use X/Y instead of α/β (#15084)

Estimated changes

Modified Mathlib/Topology/LocallyClosed.lean

modified theorem Continuous.preimage_coborder_subset

modified theorem Embedding.isLocallyClosed_iff

modified theorem Inducing.isLocallyClosed_iff

modified theorem IsLocallyClosed.image

modified theorem IsLocallyClosed.preimage

modified def IsLocallyClosed

modified theorem IsOpenMap.coborder_preimage_subset

modified theorem OpenEmbedding.coborder_preimage

modified def coborder

modified theorem coborder_preimage

modified theorem isLocallyClosed_iff_coe_preimage_of_iSup_eq_top

modified theorem isLocallyClosed_tfae