English
The sum of the cardinalities of truncatedSup over the union and the symmetric difference equals the sum over each individually.
Русский
Сумма кардинальных чисел truncatedSup по объединению и симметрическому различию равна сумме по каждому из них по отдельности.
LaTeX
$$$\#(\mathrm{truncatedSup}(\mathcal{A} \cup \mathcal{B}, s)) + #(\mathrm{truncatedSup}(\mathcal{A} \triangle \mathcal{B}, s)) = #(\mathrm{truncatedSup}(\mathcal{A}, s)) + #(\mathrm{truncatedSup}(\mathcal{B}, s))$$$
Lean4
theorem card_truncatedSup_union_add_card_truncatedSup_infs (𝒜 ℬ : Finset (Finset α)) (s : Finset α) :
#(truncatedSup (𝒜 ∪ ℬ) s) + #(truncatedSup (𝒜 ⊼ ℬ) s) = #(truncatedSup 𝒜 s) + #(truncatedSup ℬ s) :=
by
by_cases h𝒜 : s ∈ lowerClosure (𝒜 : Set <| Finset α) <;> by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)
· rw [truncatedSup_union h𝒜 hℬ, truncatedSup_infs h𝒜 hℬ]
exact card_union_add_card_inter _ _
· rw [truncatedSup_union_left h𝒜 hℬ, truncatedSup_of_notMem hℬ, truncatedSup_infs_of_notMem fun h ↦ hℬ h.2]
· rw [truncatedSup_union_right h𝒜 hℬ, truncatedSup_of_notMem h𝒜, truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1, add_comm]
·
rw [truncatedSup_of_notMem h𝒜, truncatedSup_of_notMem hℬ, truncatedSup_union_of_notMem h𝒜 hℬ,
truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1]
