English
Let c be a regular cardinal and ι a type. If the lift of the cardinality of ι is strictly below c, and for every i we have f(i) < ord(c), then the supremum of f over ι is still below ord(c).
Русский
Пусть c — регулярное кардинальное число и ι — произвольный тип. Если возведение кардинала мощности множества индексов #ι строго меньше c, и для каждого i выполняется f(i) < ord(c), то верхняя грань по i: ∑ f(i) (или sup) также меньше ord(c).
LaTeX
$$$IsRegular(c) \land \operatorname{lift}(\#\iota) < c \land \left( \forall i,\ f(i) < \operatorname{ord}(c) \right) \Rightarrow \bigsup_{i \in \iota} f(i) < \operatorname{ord}(c)$$$
Lean4
theorem iSup_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : Cardinal.lift.{v, u} #ι < c) :
(∀ i, f i < c.ord) → iSup f < c.ord :=
iSup_lt_ord_lift (by rwa [hc.cof_eq])
