mu_eq_neg_sum_Ioc_of_ne — Mathlib

English

A general form of Möbius inversion: if g(x) = ∑_{y ∈ Ici x} f(y) for all x, then for every x, f(x) = ∑_{y ∈ Ici x} μ(x,y) g(y).

Русский

Обобщённая инверсия Мёбиуса: если g(x) = ∑_{y ∈ Ici x} f(y) для всех x, тогда для каждого x выполняется f(x) = ∑_{y ∈ Ici x} μ(x,y) g(y).

LaTeX

$$$ \forall f,g, (\forall x, g x = \sum_{y \in Ici x} f y) \rightarrow \forall x, f x = \sum_{y \in Ici x} μ 𝕜 x y \cdot g y $$$

Lean4

theorem mu_eq_neg_sum_Ioc_of_ne (hab : a ≠ b) : mu 𝕜 a b = -∑ x ∈ Ioc a b, mu 𝕜 x b := by
  rw [mu_eq_mu', mu'_eq_sum_Ioc_of_ne hab]

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