Commit 2023-02-08 08:24 a43ac05d

View on Github →

feat: port Topology.Order.Hom.Basic (#2138)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Order/Hom/Basic.lean

added theorem ContinuousOrderHom.cancel_left

added theorem ContinuousOrderHom.cancel_right

added theorem ContinuousOrderHom.coe_comp

added theorem ContinuousOrderHom.coe_copy

added theorem ContinuousOrderHom.coe_id

added theorem ContinuousOrderHom.coe_toOrderHom

added def ContinuousOrderHom.comp

added theorem ContinuousOrderHom.comp_apply

added theorem ContinuousOrderHom.comp_assoc

added theorem ContinuousOrderHom.comp_id

added theorem ContinuousOrderHom.copy_eq

added theorem ContinuousOrderHom.ext

added theorem ContinuousOrderHom.id_apply

added theorem ContinuousOrderHom.id_comp

added def ContinuousOrderHom.toContinuousMap

added theorem ContinuousOrderHom.toFun_eq_coe

added structure ContinuousOrderHom