mu_ofDual

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

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

English

The dual Möbius function μ on OrderDual behaves as the reversed μ on the original order.

Русский

Дуальная функция Мёбиуса μ на OrderDual ведёт себя как обращённая μ на исходном порядке.

LaTeX

$$$ μ 𝕜 (toDual a) (toDual b) = μ 𝕜 b a $$$

Lean4

@[simp]
theorem mu_ofDual (a b : αᵒᵈ) : mu 𝕜 (ofDual a) (ofDual b) = mu 𝕜 b a :=
  (mu_toDual ..).symm

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

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

Разделы

Аффилиация

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