eulerChar_orderDual — Mathlib

English

For a finite bounded order, the Euler characteristic is defined as eulerChar 𝕜 α = μ 𝕜 ⊥ ⊤, i.e., the Möbius inversion from bottom to top.

Русский

Для конечного ограниченного порядка эйлеровская характеристика определяется как eulerChar 𝕜 α = μ 𝕜 ⊥ ⊤, то есть инверсия Моёбиуса от нижней границы к верхней.

LaTeX

$$$ \text{eulerChar } 𝕜 α = μ 𝕜 ⊥ ⊤ $$$

Lean4

@[simp]
theorem eulerChar_orderDual [BoundedOrder α] : eulerChar 𝕜 αᵒᵈ = eulerChar 𝕜 α := by
  simp [eulerChar, ← mu_toDual 𝕜 (α := α)]

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