mul_ciInf — Mathlib

English

Left-multiplication distributes over ciInf: a · (inf_i f(i)) = inf_i (a · f(i)).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_ciInf (hf : BddBelow (range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i :=
  (OrderIso.mulLeft a).map_ciInf hf

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