isPartition_of_exists_of_ne_empty

English

The union of the sets in a partition equals the entire base set.

Русский

Объединение множеств в разбиении равно всей базовой множеству.

LaTeX

$$$\\\\bigcup c = α$$$

Lean4

theorem _root_.Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty {α : Type*} {s : Set (Set α)}
    (h₁ : s.PairwiseDisjoint id) (h₂ : ∀ a : α, ∃ x ∈ s, a ∈ x) (h₃ : ∅ ∉ s) : Setoid.IsPartition s :=
  by
  refine ⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩
  intro b₁ b₂ hb₁ hb₂
  apply h₁.elim hb₁.1 hb₂.1
  simp only [Set.not_disjoint_iff]
  exact ⟨a, hb₁.2, hb₂.2⟩

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