Commit 2026-10-17 11:31 d192224e

View on Github →

chore: rename HomeomorphClass.toHomeomorph projection (#44907) to Homeomorph.ofClass, in line with #31365.

Estimated changes

Modified Mathlib/Topology/Homeomorph/Defs.lean

added def Homeomorph.ofClass

added theorem Homeomorph.ofClass_injective

deleted theorem HomeomorphClass.coe_coe

deleted def HomeomorphClass.toHomeomorph

deleted theorem HomeomorphClass.toHomeomorph_injective

Modified Mathlib/Topology/Order/MonotoneContinuity.lean