toTypeOrderBot — Mathlib

English

If c ≠ 0, the type c.ord.toType has a bottom element (is an ordered set with a least element).

Русский

Если c ≠ 0, то множество c.ord.toType имеет наименьший элемент (есть нижняя граница).

LaTeX

$$ToTypeOrderBot({\\tt c})(hc) :\\; \\text{OrderBot}(c.ord.toType)$$

Lean4

/-- If a cardinal `c` is nonzero, then `c.ord.toType` has a least element. -/
noncomputable def toTypeOrderBot {c : Cardinal} (hc : c ≠ 0) : OrderBot c.ord.toType :=
  Ordinal.toTypeOrderBot (fun h ↦ hc (ord_injective (by simpa using h)))

Похожие утверждения