Commit 2023-06-07 00:58 5caec4ba

View on Github →

feat: port Topology.Order.Hom.Esakia (#3108)

Estimated changes

Modified Mathlib.lean

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

added def ContinuousOrderHomClass.toContinuousOrderHom

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

added theorem EsakiaHom.cancel_left

added theorem EsakiaHom.cancel_right

added theorem EsakiaHom.coe_comp

added theorem EsakiaHom.coe_comp_continuousOrderHom

added theorem EsakiaHom.coe_comp_pseudoEpimorphism

added theorem EsakiaHom.coe_copy

added theorem EsakiaHom.coe_id

added theorem EsakiaHom.coe_id_continuousOrderHom

added theorem EsakiaHom.coe_id_pseudoEpimorphism

added def EsakiaHom.comp

added theorem EsakiaHom.comp_apply

added theorem EsakiaHom.comp_assoc

added theorem EsakiaHom.comp_id

added theorem EsakiaHom.copy_eq

added theorem EsakiaHom.ext

added theorem EsakiaHom.id_apply

added theorem EsakiaHom.id_comp

added theorem EsakiaHom.toContinuousOrderHom_coe

added theorem EsakiaHom.toFun_eq_coe

added def EsakiaHom.toPseudoEpimorphism

added structure EsakiaHom

added theorem PseudoEpimorphism.cancel_left

added theorem PseudoEpimorphism.cancel_right

added theorem PseudoEpimorphism.coe_comp

added theorem PseudoEpimorphism.coe_comp_orderHom

added theorem PseudoEpimorphism.coe_copy

added theorem PseudoEpimorphism.coe_id

added theorem PseudoEpimorphism.coe_id_orderHom

added def PseudoEpimorphism.comp

added theorem PseudoEpimorphism.comp_apply

added theorem PseudoEpimorphism.comp_assoc

added theorem PseudoEpimorphism.comp_id

added theorem PseudoEpimorphism.copy_eq

added theorem PseudoEpimorphism.ext

added theorem PseudoEpimorphism.id_apply

added theorem PseudoEpimorphism.id_comp

added theorem PseudoEpimorphism.toFun_eq_coe

added structure PseudoEpimorphism