Commit 2022-01-28 00:40 bac0f55e

View on Github →

chore(order/conditionally_complete_lattice): move code to a new file (#11698) This is the first step towards adding a complete_lattice instance for Icc/interval.

Estimated changes

Modified src/algebra/order/nonneg.lean

Created src/order/complete_lattice_intervals.lean

added theorem Inf_within_of_ord_connected

added theorem Sup_within_of_ord_connected

added theorem subset_Inf_def

added theorem subset_Inf_of_within

added theorem subset_Sup_def

added theorem subset_Sup_of_within

Modified src/order/conditionally_complete_lattice.lean

deleted theorem Inf_within_of_ord_connected

deleted theorem Sup_within_of_ord_connected

deleted theorem subset_Inf_def

deleted theorem subset_Inf_of_within

deleted theorem subset_Sup_def

deleted theorem subset_Sup_of_within

Modified src/topology/algebra/ordered/intermediate_value.lean