iInf_unique

Mathlib.Order.CompleteLattice.Basic

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

English

If ι has a unique element, the infimum of f over ι equals f of that unique element: ⨅ i, f(i) = f(default).

Русский

Если ι имеет единственный элемент, то ⨅ i, f(i) = f(единственный элемент).

LaTeX

$$$\\\\iInf i, f(i) = f\\\$default\\\$$$$

Lean4

theorem iInf_unique [Unique ι] (f : ι → α) : ⨅ i, f i = f default := by
  simp only [congr_arg f (Unique.eq_default _), iInf_const]

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

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

Разделы

Аффилиация

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