iUnion_eq_empty — Mathlib

English

The union of a family of sets equals the empty set if and only if each member of the family is empty: ⋃ i, s i = ∅ ↔ ∀ i, s i = ∅.

Русский

Объединение семейства множеств равно пустому множеству тогда и только тогда, когда каждое множество в семье пусто: ⋃ i, s i = ∅ ↔ ∀ i, s i = ∅.

LaTeX

$$$$\\bigcup_{i} s_i = \\emptyset \\;\\iff\\; \\forall i, \\; s_i = \\emptyset$$$$

Lean4

@[simp]
theorem iUnion_eq_empty : ⋃ i, s i = ∅ ↔ ∀ i, s i = ∅ :=
  iSup_eq_bot

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