sum_Icc_mu_left — Mathlib

English

Summing μ over the left side of an interval yields 1 if a=b and 0 otherwise: ∑_{x ∈ Icc a b} μ(x,b) = δ_{a,b}.

Русский

Сумма μ по левой части интервала равна 1, если a=b, и 0 иначе: ∑_{x ∈ Icc a b} μ(x,b) = δ_{a,b}.

LaTeX

$$$ \sum_{x \in Icc a b} μ 𝕜 x b = \begin{cases} 1, & a=b, \\ 0, & a≠b. \end{cases}$$$

Lean4

theorem sum_Icc_mu_left (a b : α) : ∑ x ∈ Icc a b, mu 𝕜 x b = if a = b then 1 else 0 := by
  rw [mu_eq_mu', sum_Icc_mu'_left]

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