smul_indicator_one_apply — Mathlib

English

Let s be a subset of α and r ∈ R. Then r acting on the indicator of the constant function 1 on α satisfies r • s.indicator (1) a = s.indicator (λ x, r) a for all a ∈ α.

Русский

Пусть s ⊆ α и r ∈ R. Тогда действие r на индикатор константной функции 1 дает: r • s.indicator(1) a = s.indicator(λx, r) a для всех a ∈ α.

LaTeX

$$$$ r \\cdot s\\,\\mathrm{indicator}(1)(a) = s\\,\\mathrm{indicator}(\\lambda x. r)(a). $$$$

Lean4

theorem smul_indicator_one_apply (s : Set α) (r : R) (a : α) :
    r • s.indicator (1 : α → R) a = s.indicator (fun _ ↦ r) a := by
  simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]

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