iSup_mul_distrib — Mathlib

English

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

Русский

Пусть α — полугруппа с полным упорядочением и IsQuantale. Тогда (iSup f i) · x = iSup (f i · x).

LaTeX

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

Lean4

@[to_additive]
theorem iSup_mul_distrib : (⨆ i, f i) * x = ⨆ i, f i * x := by rw [iSup, sSup_mul_distrib, iSup_range]

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