iSup_eq_of_range_eq

Mathlib.SetTheory.Ordinal.Family

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

English

Equality of range implies equality of supremums for ordinal-valued functions.

Русский

Равенство диапазонов порождает равенство верхних границ для функций-ordinals.

LaTeX

$$$\mathrm{range}\ f = \mathrm{range}\ g \Rightarrow iSup\ f = iSup\ g$$$

Lean4

theorem iSup_eq_of_range_eq {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} (h : Set.range f = Set.range g) :
    iSup f = iSup g :=
  congr_arg _ h

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

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

Разделы

Аффилиация

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