Commit 2025-04-10 03:41 6a90bb42

View on Github →

chore: move some results out of Topology.Homeomorph.Lemmas (#23861) Mathlib.Topology.Homeomorph.Lemmas is a grab-bag of results involving homeomorphisms, but some of them can move earlier at no cost.

Estimated changes

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

Modified Mathlib/Topology/Algebra/Constructions.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

Modified Mathlib/Topology/Algebra/MulAction.lean

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

Modified Mathlib/Topology/Homeomorph/Defs.lean

added theorem Homeomorph.comap_nhds_eq

added theorem Homeomorph.map_nhds_eq

added theorem Homeomorph.nhds_eq_comap

added theorem Homeomorph.symm_map_nhds_eq

added theorem IsHomeomorph.comp

added structure IsHomeomorph

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

deleted theorem Homeomorph.comap_nhds_eq

deleted theorem Homeomorph.map_nhds_eq

deleted theorem Homeomorph.nhds_eq_comap

deleted theorem Homeomorph.symm_map_nhds_eq

deleted theorem IsHomeomorph.comp

deleted structure IsHomeomorph

Modified Mathlib/Topology/MetricSpace/Isometry.lean

Modified Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/UniformSpace/Equiv.lean