Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Inf_within_of_ord_connected

Modification history

2022-01-28 00:40
src/order/complete_lattice_intervals.lean
chore(order/conditionally_complete_lattice): move code to a new file (#11698) …
Modified Inf_within_of_ord_connectedView on Github →
2020-09-09 13:02
src/order/conditionally_complete_lattice.lean
feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for `ord_connected` subset (#3991) …
Added Inf_within_of_ord_connectedView on Github →