sSup_apply

Mathlib.Order.Hom.Order

URI: https://scilib.ai/kg/mathlib#OrderHom.sSup_apply

English

The supremum over a set of order-preserving maps, applied to x, equals the supremum over the set of maps of their values at x.

Русский

Супремум над множеством отображений применим к x как супремум их значений на x.

LaTeX

$$$sSup\; s\; x = \sup_{f \in s} f(x).$$$

Lean4

@[simp]
theorem sSup_apply [CompleteLattice β] (s : Set (α →o β)) (x : α) : sSup s x = ⨆ f ∈ s, (f :) x :=
  rfl

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

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

Разделы

Аффилиация

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