Commit 2020-06-01 05:31 7263917e

View on Github →

chore(order/complete_lattice): redefine ord_continuous (#2886) Redefine ord_continuous using is_lub to ensure that the definition makes sense for conditionally_complete_lattices.

Estimated changes

Modified src/order/bounds.lean

Modified src/order/complete_lattice.lean

deleted theorem ord_continuous.mono

deleted theorem ord_continuous.sup

deleted def ord_continuous

Created src/order/ord_continuous.lean

added theorem left_ord_continuous.coe_to_le_order_embedding

added theorem left_ord_continuous.coe_to_lt_order_embedding

added theorem left_ord_continuous.comp

added theorem left_ord_continuous.le_iff

added theorem left_ord_continuous.lt_iff

added theorem left_ord_continuous.map_Sup'

added theorem left_ord_continuous.map_Sup

added theorem left_ord_continuous.map_cSup

added theorem left_ord_continuous.map_csupr

added theorem left_ord_continuous.map_is_greatest

added theorem left_ord_continuous.map_sup

added theorem left_ord_continuous.map_supr

added theorem left_ord_continuous.mono

added def left_ord_continuous.to_le_order_embedding

added def left_ord_continuous.to_lt_order_embedding

added def left_ord_continuous

added theorem right_ord_continuous.coe_to_le_order_embedding

added theorem right_ord_continuous.coe_to_lt_order_embedding

added theorem right_ord_continuous.comp

added theorem right_ord_continuous.le_iff

added theorem right_ord_continuous.lt_iff

added theorem right_ord_continuous.map_Inf'

added theorem right_ord_continuous.map_Inf

added theorem right_ord_continuous.map_cInf

added theorem right_ord_continuous.map_cinfi

added theorem right_ord_continuous.map_inf

added theorem right_ord_continuous.map_infi

added theorem right_ord_continuous.map_is_least

added theorem right_ord_continuous.mono

added def right_ord_continuous.to_le_order_embedding

added def right_ord_continuous.to_lt_order_embedding

added def right_ord_continuous