blsub_one

Mathlib.SetTheory.Ordinal.Family

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

English

Blsub on 1 with f is equal to succ(f(0)).

Русский

Blsub на 1: blsub 1 f = succ(f(0)).

LaTeX

$$$ \\operatorname{blsub}(1,f) = \\operatorname{succ}(f(0)) $$$

Lean4

@[simp]
theorem blsub_one (f : ∀ a < (1 : Ordinal), Ordinal) : blsub 1 f = succ (f 0 zero_lt_one) :=
  bsup_one _

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

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

Разделы

Аффилиация

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