smul_dirac_apply — Mathlib

English

For a scalar a and point b, the scalar multiple of the Dirac outer measure satisfies (a • dirac b)(s) = a if b ∈ s and 0 otherwise.

Русский

Для скаляра a и точки b, умножение на Dirac-меру даёт (a • dirac b)(s) = a при включении b в s, и 0 иначе.

LaTeX

$$$ (a \cdot dirac\ b)(s) = a \cdot \mathbf{1}_{s}(b) $$$

Lean4

theorem smul_dirac_apply (a : ℝ≥0∞) (b : α) (s : Set α) : (a • dirac b) s = indicator s (fun _ => a) b := by
  simp only [smul_apply, smul_eq_mul, dirac_apply, ← indicator_mul_right _ fun _ => a, mul_one]

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