infSum_eq_one — Mathlib

English

Same statement as above: if 𝒜 is nonempty and ∅ ∉ 𝒜, then infSum 𝒜 = 1.

Русский

То же утверждение: если 𝒜 непусто и ∅ ∉ 𝒜, то infSum 𝒜 = 1.

LaTeX

$$$\infSum 𝒜 = 1$$$

Lean4

/-- The **Ahlswede-Zhang Identity**. -/
theorem infSum_eq_one (h𝒜₁ : 𝒜.Nonempty) (h𝒜₀ : ∅ ∉ 𝒜) : infSum 𝒜 = 1 :=
  by
  rw [← compls_compls 𝒜, eq_sub_of_add_eq (infSum_compls_add_supSum _), supSum_of_univ_notMem h𝒜₁.compls,
    add_sub_cancel_left]
  simpa

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