mathlib

a1ce53c0 - refactor(set_theory/ordinal/basic): `ordinal.min` → `infi` (#14707)

refactor(set_theory/ordinal/basic): `ordinal.min` → `infi` (#14707) We ditch `ordinal.min` (which is really just `infi`). Apart from this, we add some missing theorems on conditionally complete lattices with a bottom element.