Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.Inf_eq_omin

Modification history

2022-02-15 15:52
src/set_theory/ordinal.lean
refactor(set_theory/ordinal_arithmetic): `omin` → `Inf` (#11867) …
Deleted ordinal.Inf_eq_ominView on Github →
2021-09-18 13:22
src/set_theory/ordinal.lean
feat(set_theory/ordinal): add conditionally_complete_linear_order_bot instance (#9266) …
Added ordinal.Inf_eq_ominView on Github →