lsub_notMem_range

Mathlib.SetTheory.Ordinal.Family

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

English

Lsub f is not an element of the range of f: lsub f ∉ Range f.

Русский

lsub f не принадлежит образу f; lsub f ∉ Range(f).

LaTeX

$$lsub f ∉ \operatorname{Range}(f)$$

Lean4

theorem lsub_notMem_range {ι} (f : ι → Ordinal) : lsub f ∉ Set.range f := fun ⟨i, h⟩ => h.not_lt (lt_lsub f i)

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

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

Разделы

Аффилиация

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