Mathlib v3 is deprecated. Go to Mathlib v4

Theorem not_mem_of_lt_cInf

Modification history

2021-09-18 13:22

src/order/conditionally_complete_lattice.lean

feat(set_theory/ordinal): add conditionally_complete_linear_order_bot instance (#9266) …

Added not_mem_of_lt_cInf View on Github →