mul_iSup_distrib — Mathlib

English

Let α be a semigroup with CompleteLattice structure and IsQuantale. Then for every x and f: i → α, x · (iSup f i) = iSup (x · f i).

Русский

Пусть α — полугруппа с полным образованием и IsQuantale. Тогда для любого x и функции f: i → α выполняется x · (iSup f(i)) = iSup (x · f(i)).

LaTeX

$$$\\\\forall x \\\\in \\\\alpha \\\\forall f \\\\colon \\\\iota \\\\to \\\\alpha,\n x \\\\cdot (\\\\iSup f) = \\\\iSup (\\\\lambda i, x \\\\cdot f(i)).$$$

Lean4

@[to_additive]
theorem mul_iSup_distrib : x * ⨆ i, f i = ⨆ i, x * f i := by rw [iSup, mul_sSup_distrib, iSup_range]

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