Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 13:18 7de8137d

View on Github →

feat(topology/order/hom): Continuous order homomorphisms (#12012) Define continuous monotone functions, aka continuous order homomorphisms, aka Priestley homomorphisms, with notation α →Co β.

Estimated changes

Modified src/topology/continuous_function/basic.lean

Created src/topology/order/hom/basic.lean

added theorem continuous_order_hom.cancel_left

added theorem continuous_order_hom.cancel_right

added theorem continuous_order_hom.coe_comp

added theorem continuous_order_hom.coe_id

added def continuous_order_hom.comp

added theorem continuous_order_hom.comp_apply

added theorem continuous_order_hom.comp_assoc

added theorem continuous_order_hom.comp_id

added theorem continuous_order_hom.ext

added theorem continuous_order_hom.id_apply

added theorem continuous_order_hom.id_comp

added def continuous_order_hom.to_continuous_map

added theorem continuous_order_hom.to_fun_eq_coe

added structure continuous_order_hom