lsub_pos — Mathlib

English

Let I be a nonempty index set and f: I → Ordinal. Then the least upper bound of the successors of f, namely lsub f, is strictly greater than 0; in particular lsub f > 0.

Русский

Пусть I непустый множество индексов и функция f: I → Ordinal. Тогда наименьшая верхняя грань последовательностей, заданных как succ(f(i)), превосходит 0, то есть lsub f > 0.

LaTeX

$$$0 < \operatorname{lsub} f$$$

Lean4

theorem lsub_pos {ι} [h : Nonempty ι] (f : ι → Ordinal) : 0 < lsub f :=
  h.elim fun i => (Ordinal.zero_le _).trans_lt (lt_lsub f i)

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