nonempty_compl_range

Mathlib.SetTheory.Ordinal.Family

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

English

For any f: ι → Ordinal, the complement of its range is nonempty.

Русский

Для любого f: ι → Ordinal дополнение диапазона не пусто.

LaTeX

$$(Set.range f)ᶜ.Nonempty$$

Lean4

theorem nonempty_compl_range {ι : Type u} (f : ι → Ordinal.{max u v}) : (Set.range f)ᶜ.Nonempty :=
  ⟨_, lsub_notMem_range f⟩

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

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

Разделы

Аффилиация

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