sUnion_eq_univ — Mathlib

English

If c is a partition of α, then the union of its blocks is the whole α.

Русский

Если c является разбиением α, то объединение его блоков равно всей α.

LaTeX

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

Lean4

theorem sUnion_eq_univ {c : Set (Set α)} (hc : IsPartition c) : ⋃₀ c = Set.univ :=
  Set.eq_univ_of_forall fun x =>
    Set.mem_sUnion.2 <|
      let ⟨t, ht⟩ := hc.2 x
      ⟨t, by
        simp only at ht
        tauto⟩

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