English
If 𝒜 is a nonempty finite family of subsets of α and does not contain the empty set, then infSum 𝒜 = 1.
Русский
Если 𝒜 — непустое конечное семейство подмножеств α и не содержит пустое множество, то infSum 𝒜 = 1.
LaTeX
$$$\infSum 𝒜 = 1$$$
Lean4
theorem supSum_of_univ_notMem (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) :
supSum 𝒜 = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹ :=
by
set m := 𝒜.card with hm
clear_value m
induction m using Nat.strongRecOn generalizing 𝒜 with
| ind m ih => _
replace ih := fun 𝒜 h𝒜 h𝒜₁ h𝒜₂ ↦ @ih _ h𝒜 𝒜 h𝒜₁ h𝒜₂ rfl
obtain ⟨a, rfl⟩ | h𝒜₃ := h𝒜₁.exists_eq_singleton_or_nontrivial
· refine supSum_singleton ?_
simpa [eq_comm] using h𝒜₂
cases m
· cases h𝒜₁.card_pos.ne hm
obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_succ.1 hm.symm
have h𝒜 : 𝒜.Nonempty := nonempty_iff_ne_empty.2 (by rintro rfl; simp at h𝒜₃)
rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
· exact card_image_le.trans_lt (lt_add_one _)
· exact h𝒜.image _
· simpa using fun _ ↦ ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂
· exact lt_add_one _
· exact h𝒜
· exact fun h ↦ h𝒜₂ (mem_insert_of_mem h)
