bsup_eq_blsub

Mathlib.SetTheory.Ordinal.Family

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

← MathLib Explorer

English

As a definitional fact, bsup equals blsub when indexing the same way: bsup o f = blsub o f.

Русский

Определение даёт равенство: bsup o f = blsub o f.

LaTeX

$$$\operatorname{bsup}\!\,(o) f = \operatorname{blsub}\!\,(o) f$$$

Lean4

@[simp]
theorem bsup_eq_blsub (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) :
    (bsup.{_, v} o fun a ha => succ (f a ha)) = blsub.{_, v} o f :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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