mul_ciSup — Mathlib

English

Left-multiplication distributes over ciSup: a · (sup_i f(i)) = sup_i (a · f(i)).

Русский

Левое умножение распределяет над ciSup: a · sup_i f(i) = sup_i (a · f(i)).

LaTeX

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

Lean4

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

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