Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-25 01:36 a1ce53c0

View on Github →

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.

Estimated changes

added theorem cinfi_le'
added theorem infi_mem
added theorem le_cinfi_iff'
modified theorem cardinal.ord_eq
added theorem cardinal.ord_eq_Inf
deleted theorem cardinal.ord_eq_min
modified theorem cardinal.ord_le_type
deleted theorem ordinal.le_min
deleted theorem ordinal.lift_min
deleted def ordinal.min
deleted theorem ordinal.min_eq
deleted theorem ordinal.min_le