iSupIndep_pempty

Mathlib.Order.SupIndep

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

English

The iSupIndep property holds for all functions from the unit-extended empty type PEmpty into α as well.

Русский

Свойство iSupIndep сохраняется для отображений из PEmpty в α.

LaTeX

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

Lean4

@[simp]
theorem iSupIndep_pempty (t : PEmpty → α) : iSupIndep t :=
  nofun

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

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

Разделы

Аффилиация

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