mu_self

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

URI: https://scilib.ai/kg/mathlib#IncidenceAlgebra.mu_self

English

If a ≠ b, μ(a,b) = - ∑_{x ∈ Ico a b} μ(a,x).

Русский

Если a ≠ b, то μ(a,b) = −∑_{x ∈ Ico a b} μ(a,x).

LaTeX

$$$ a \neq b \Rightarrow μ 𝕜 a b = -\sum_{x \in Ico a b} μ 𝕜 a x $$$

Lean4

@[simp]
theorem mu_self (a : α) : mu 𝕜 a a = 1 := by simp [mu_apply]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru