English
The infSum satisfies a union identity: infSum(𝒜 ∪ ℬ) + infSum(𝒜 ⊼ ℬ) = infSum 𝒜 + infSum ℬ.
Русский
InfSum удовлетворяет тождеству по объединению: infSum(𝒜 ∪ ℬ) + infSum(𝒜 ⊼ ℬ) = infSum 𝒜 + infSum ℬ.
LaTeX
$$$\mathrm{infSum}(\mathcal{A} \cup \mathcal{B}) + \mathrm{infSum}(\mathcal{A} \triangle \mathcal{B}) = \mathrm{infSum}(\mathcal{A}) + \mathrm{infSum}(\mathcal{B})$$$
Lean4
theorem infSum_union_add_infSum_sups (𝒜 ℬ : Finset (Finset α)) :
infSum (𝒜 ∪ ℬ) + infSum (𝒜 ⊻ ℬ) = infSum 𝒜 + infSum ℬ :=
by
unfold infSum
rw [← sum_add_distrib, ← sum_add_distrib, sum_congr rfl fun s _ ↦ _]
simp_rw [← add_div, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups]
simp