Commit 2023-02-10 07:10 d1691b84

View on Github →

feat: port Topology.Hom.Open (#2172)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Hom/Open.lean

added theorem ContinuousOpenMap.cancel_left

added theorem ContinuousOpenMap.cancel_right

added theorem ContinuousOpenMap.coe_comp

added theorem ContinuousOpenMap.coe_copy

added theorem ContinuousOpenMap.coe_id

added theorem ContinuousOpenMap.coe_toContinuousMap

added def ContinuousOpenMap.comp

added theorem ContinuousOpenMap.comp_apply

added theorem ContinuousOpenMap.comp_assoc

added theorem ContinuousOpenMap.comp_id

added theorem ContinuousOpenMap.copy_eq

added theorem ContinuousOpenMap.ext

added theorem ContinuousOpenMap.id_apply

added theorem ContinuousOpenMap.id_comp

added theorem ContinuousOpenMap.toFun_eq_coe

added structure ContinuousOpenMap