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