smul_iSup — Mathlib

English

For a scalar action of R on ENat, c • ⨆ i, f i = ⨆ i, c • f i.

Русский

При действии скаляра на ENat выполняется: c • ⨆ i, f i = ⨆ i, c • f i.

LaTeX

$$$ \text{[SMul } R \ ENat] \to \text{[IsScalarTower } R \ ENat \ ENat] \rightarrow c \cdot \big( \big( \bigvee_i f_i \big) \big) = \big( \bigvee_i (c \cdot f_i) \big) $$$

Lean4

theorem smul_iSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) : c • ⨆ i, f i = ⨆ i, c • f i := by
  simpa using mul_iSup (c • 1) f

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