Commit 2020-09-09 13:02 40de35aa

View on Github →

feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for ord_connected subset (#3991) If α is densely_ordered, then so is the subtype s, for any ord_connected subset s of α. Same result for order_topology. Same result for conditionally_complete_linear_order, under the hypothesis inhabited s.

Estimated changes

Modified src/data/set/intervals/ord_connected.lean

Modified src/order/basic.lean

added theorem strict_mono_coe

Modified src/order/conditionally_complete_lattice.lean

added theorem Inf_within_of_ord_connected

added theorem Sup_within_of_ord_connected

added theorem monotone.cInf_image_le

added theorem monotone.cSup_image_le

added theorem monotone.le_cInf_image

added theorem monotone.le_cSup_image

added theorem subset_Inf_def

added theorem subset_Inf_of_within

added theorem subset_Sup_def

added theorem subset_Sup_of_within

Modified src/topology/algebra/ordered.lean