English
A similar cardinality identity holds for truncatedInf with union and symmetric difference.
Русский
Похожая тождественность кардиналов справедлива для truncatedInf при объединении и симметрическом различии.
LaTeX
$$$\#(\mathrm{truncatedInf}(\mathcal{A} \cup \mathcal{B}, s)) + #(\mathrm{truncatedInf}(\mathcal{A} \triangle \mathcal{B}, s)) = #(\mathrm{truncatedInf}(\mathcal{A}, s)) + #(\mathrm{truncatedInf}(\mathcal{B}, s))$$$
Lean4
theorem card_truncatedInf_union_add_card_truncatedInf_sups (𝒜 ℬ : Finset (Finset α)) (s : Finset α) :
#(truncatedInf (𝒜 ∪ ℬ) s) + #(truncatedInf (𝒜 ⊻ ℬ) s) = #(truncatedInf 𝒜 s) + #(truncatedInf ℬ s) :=
by
by_cases h𝒜 : s ∈ upperClosure (𝒜 : Set <| Finset α) <;> by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)
· rw [truncatedInf_union h𝒜 hℬ, truncatedInf_sups h𝒜 hℬ]
exact card_inter_add_card_union _ _
· rw [truncatedInf_union_left h𝒜 hℬ, truncatedInf_of_notMem hℬ, truncatedInf_sups_of_notMem fun h ↦ hℬ h.2]
· rw [truncatedInf_union_right h𝒜 hℬ, truncatedInf_of_notMem h𝒜, truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1, add_comm]
·
rw [truncatedInf_of_notMem h𝒜, truncatedInf_of_notMem hℬ, truncatedInf_union_of_notMem h𝒜 hℬ,
truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1]
