blsub_eq_lsub

Mathlib.SetTheory.Ordinal.Family

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

English

For any o and f, blsub o f equals lsub of the corresponding family.

Русский

Для любых o и f, blsub o f равно lsub соответствующего семейства.

LaTeX

$$$\operatorname{blsub}(o,f) = \operatorname{lsub}(\text{familyOfBFamily } f)$$$

Lean4

@[simp]
theorem blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : blsub.{_, v} _ (bfamilyOfFamily f) = lsub.{_, v} f :=
  blsub_eq_lsub' _ _

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

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

Разделы

Аффилиация

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