ciInf_mul — Mathlib

English

Infimum commutes with right-multiplication: (inf_i f(i))·a = inf_i (f(i)·a).

Русский

Нижняя грань (inf) коммутирует с правым умножением: (inf_i f(i))·a = inf_i (f(i)·a).

LaTeX

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

Lean4

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

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