Def Homeomorph.toContinuousMap

Modification history

2024-10-18 10:35

Mathlib/Topology/ContinuousMap/Basic.lean

chore(Topology): deprecate `Homeomorph.toContinuousMap` (#17714) …

Deleted Homeomorph.toContinuousMap View on Github →

2023-02-06 02:37

Mathlib/Topology/ContinuousFunction/Basic.lean

feat: port Topology.ContinuousFunction.Basic (#2053)

Added Homeomorph.toContinuousMap View on Github →