support_const_smul_of_ne_zero — Mathlib

English

The indicator of the pointwise product r • f is the product of r with the indicator of f.

Русский

Индикатор точки произведения r • f равен произведению r на индикатор f.

LaTeX

$$$ \mathbf{1}_{s}(r \cdot f) = r \cdot \mathbf{1}_{s}(f) $$$

Lean4

theorem support_const_smul_of_ne_zero [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (c : R) (g : α → M)
    (hc : c ≠ 0) : support (c • g) = support g :=
  ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or]

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