infSum_union_add_infSum_sups — Mathlib

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

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