Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-22 09:42 5826b2fb

View on Github →

feat(topology/order/hom/esakia): Esakia morphisms (#12241) Define pseudo-epimorphisms and Esakia morphisms following the hom refactor.

Estimated changes

added theorem esakia_hom.cancel_left
added theorem esakia_hom.coe_comp
added theorem esakia_hom.coe_id
added def esakia_hom.comp
added theorem esakia_hom.comp_apply
added theorem esakia_hom.comp_assoc
added theorem esakia_hom.comp_id
added theorem esakia_hom.ext
added theorem esakia_hom.id_apply
added theorem esakia_hom.id_comp
added structure esakia_hom
added theorem pseudo_epimorphism.ext
added structure pseudo_epimorphism