iInf_eq_top_of_isEmpty

Mathlib.Data.ENat.Lattice

URI: https://scilib.ai/kg/mathlib#ENat.iInf_eq_top_of_isEmpty

English

If the index type ι is empty, then the infimum over i of (f i) in ENat equals the top element.

Русский

Если индексный тип ι пуст, то инфимум по i от (f i) в ENat равен верхнему элементу.

LaTeX

$$$[IsEmpty \iota] \;: \; \inf_i (f(i) : \mathbb{N}_\infty) = \top$$$

Lean4

@[simp]
theorem iInf_eq_top_of_isEmpty [IsEmpty ι] : ⨅ i, (f i : ℕ∞) = ⊤ :=
  iInf_coe_eq_top.mpr ‹_›

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

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

Разделы

Аффилиация

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