iSup_apply — Mathlib

English

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

Русский

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

LaTeX

$$$(\sup_i f_i)\, x = \sup_i (f_i\, x).$$$

Lean4

theorem iSup_apply {ι : Sort*} [CompleteLattice β] (f : ι → α →o β) (x : α) : (⨆ i, f i) x = ⨆ i, f i x :=
  (sSup_apply _ _).trans iSup_range

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