sup_add_inf_eq_add — Mathlib

English

In a FactorSet, the join and meet interact with addition via a distributive-like identity: a ⊔ b + a ⊓ b = a + b.

Русский

В FactorSet выполняется тождество схожее с дистрибутивностью: верхняя и нижняя объединения вместе дают обычное сложение.

LaTeX

$$$a \vee b + a \wedge b = a + b$ in FactorSet.$$

Lean4

theorem sup_add_inf_eq_add [DecidableEq (Associates α)] : ∀ a b : FactorSet α, a ⊔ b + a ⊓ b = a + b
  | ⊤, b => show ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b by simp
  | a, ⊤ => show a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤ by simp
  | WithTop.some a, WithTop.some b =>
    show (a : FactorSet α) ⊔ b + (a : FactorSet α) ⊓ b = a + b
      by
      rw [← WithTop.coe_sup, ← WithTop.coe_inf, ← WithTop.coe_add, ← WithTop.coe_add, WithTop.coe_eq_coe]
      exact Multiset.union_add_inter _ _

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