sUnion_eq_univ_iff — Mathlib

English

For c ⊆ Set α, the union over c equals univ if and only if every a ∈ α lies in some b ∈ c: ⋃₀ c = univ ↔ ∀ a, ∃ b ∈ c, a ∈ b.

Русский

Для c ⊆ Set α объединение над c равно univ тогда и только тогда каждый a ∈ α принадлежит некоторому b ∈ c.

LaTeX

$$$$ \\bigcup c = \\text{univ} \\;\\iff\\; \\forall a, \\exists b \\in c, a \\in b. $$$$

Lean4

theorem sUnion_eq_univ_iff {c : Set (Set α)} : ⋃₀ c = univ ↔ ∀ a, ∃ b ∈ c, a ∈ b := by
  simp only [eq_univ_iff_forall, mem_sUnion]
    -- classical

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