mu_apply — Mathlib

English

The explicit recursion for μ: μ(a,b) = 1 if a=b; otherwise μ(a,b) = - ∑_{x ∈ Ico(a,b)} μ(a,x).

Русский

Явная рекурсия для μ: μ(a,b) = 1 при a=b; иначе μ(a,b) = −∑_{x ∈ Ico(a,b)} μ(a,x).

LaTeX

$$$ μ 𝕜 a b = \begin{cases} 1, & a=b, \\ -\sum_{x \in Ico(a,b)} μ 𝕜 a x, & a \neq b. \end{cases}$$$

Lean4

theorem mu_apply (a b : α) : mu 𝕜 a b = if a = b then 1 else -∑ x ∈ Ico a b, mu 𝕜 a x := by
  rw [mu, coe_mk, muFun_apply, sum_attach]

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