blsub_pos

Mathlib.SetTheory.Ordinal.Family

URI: https://scilib.ai/kg/mathlib#Ordinal.blsub_pos

English

If o > 0, then blsub o f is positive provided f is defined.

Русский

Если o > 0, то при определённости f положительно, т.е. blsub o f > 0.

LaTeX

$$$ o > 0 \\Rightarrow (\\exists a < o, f(a) > 0) \\Rightarrow 0 < \\operatorname{blsub}(o,f) $$$

Lean4

theorem blsub_pos {o : Ordinal} (ho : 0 < o) (f : ∀ a < o, Ordinal) : 0 < blsub o f :=
  (Ordinal.zero_le _).trans_lt (lt_blsub f 0 ho)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru