inf'_singleton

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.inf'_singleton

English

The infimum over a singleton {b} is simply f(b).

Русский

Инфимум над одиночным множеством {b} равен f(b).

LaTeX

$$$\\inf'_{\\{b\\}} f = f(b)$$$

Lean4

@[simp]
theorem inf'_singleton {b : β} : ({ b } : Finset β).inf' (singleton_nonempty _) f = f b :=
  rfl

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

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

Разделы

Аффилиация

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