iSupIndep_empty

Mathlib.Order.SupIndep

URI: https://scilib.ai/kg/mathlib#iSupIndep_empty

English

The iSupIndep property holds for all functions from the empty type.

Русский

Свойство iSupIndep выполняется для любых отображений из пустого типа.

LaTeX

$$iSupIndep (t : Empty → α)$$

Lean4

@[simp]
theorem iSupIndep_empty (t : Empty → α) : iSupIndep t :=
  nofun

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

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

Разделы

Аффилиация

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