supSum_union_add_supSum_infs — Mathlib

English

The supSum satisfies a union identity: supSum(𝒜 ∪ ℬ) + supSum(𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ.

Русский

SupSum удовлетворяет тождеству по объединению: supSum(𝒜 ∪ ℬ) + supSum(𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ.

LaTeX

$$$\mathrm{supSum}(\mathcal{A} \cup \mathcal{B}) + \mathrm{supSum}(\mathcal{A} \triangle \mathcal{B}) = \mathrm{supSum}(\mathcal{A}) + \mathrm{supSum}(\mathcal{B})$$$

Lean4

theorem supSum_union_add_supSum_infs (𝒜 ℬ : Finset (Finset α)) :
    supSum (𝒜 ∪ ℬ) + supSum (𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ :=
  by
  unfold supSum
  rw [← sum_add_distrib, ← sum_add_distrib, sum_congr rfl fun s _ ↦ _]
  simp_rw [← add_div, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs]
  simp

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