ciInf_unique

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

If the index type has a unique element, iInf f equals f at that unique element.

Русский

Если множество индексов имеет единственный элемент, iInf f равен f(уникальному элементу).

LaTeX

$$iInf f = f(default) (when Unique ι)$$

Lean4

@[simp]
theorem ciInf_unique [Unique ι] {s : ι → α} : ⨅ i, s i = s default :=
  ciSup_unique (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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