iInf_empty

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#WithTop.iInf_empty

English

The infimum over an empty index set of a function into WithTop α is the top element.

Русский

Не существует индексов; инфимум по пустому множеству равен верхнему элементу.

LaTeX

$$$\displaystyle \inf_i f(i) = \top$$$

Lean4

@[simp]
theorem iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) : ⨅ i, f i = ⊤ := by
  rw [iInf, range_eq_empty, WithTop.sInf_empty]

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

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

Разделы

Аффилиация

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