sigma_eq_empty_iff — Mathlib

English

Let s be a subset of indices and t(i) a family of sets. The sigma-sum s.sigma t is empty exactly when every t(i) is empty for i in s.

Русский

Пусть s — подмножество индексов, а t(i) — семейство множеств. Сигма-произведение s.sigma t пусто тогда и только тогда, когда для каждого i ∈ s множества t(i) пусты.

LaTeX

$$$ s \\sigma t = \\emptyset \\iff \\forall i \\in s,\\ t(i) = \\emptyset $$$

Lean4

theorem sigma_eq_empty_iff : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ :=
  not_nonempty_iff_eq_empty.symm.trans <|
    sigma_nonempty_iff.not.trans <| by simp only [not_nonempty_iff_eq_empty, not_and, not_exists]

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