ciSup_mul — Mathlib

English

The supremum commutes with right-multiplication by any fixed element: (sup_i f(i))·a = sup_i (f(i)·a).

Русский

Грань наибольшего элемента коммутирует справа с умножением на фиксированный элемент: (sup_i f(i))·a = sup_i (f(i)·a).

LaTeX

$$$\forall \iota, G,\ [MulRightMono G],\ BddAbove(\mathrm{range}\ f) \Rightarrow \forall a\in G, (\sup_i f(i)) \cdot a = \sup_i (f(i) \cdot a)$$$

Lean4

@[to_additive]
theorem ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
  (OrderIso.mulRight a).map_ciSup hf

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