iInf_of_empty

Mathlib.Data.Nat.Lattice

URI: https://scilib.ai/kg/mathlib#Nat.iInf_of_empty

English

For any ι with IsEmpty ι, iInf f = 0 for any f: ι → ℕ.

Русский

Для любой множества индексов ι с условием IsEmpty ι выполняется iInf f = 0 для любой функции f: ι → ℕ.

LaTeX

$$$\\text{For all } ι \\text{ with } \\text{IsEmpty } ι, \\ iInf f = 0$$$

Lean4

@[simp]
theorem iInf_of_empty {ι : Sort*} [IsEmpty ι] (f : ι → ℕ) : iInf f = 0 := by rw [iInf_of_isEmpty, sInf_empty]

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

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

Разделы

Аффилиация

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