sUnion_disjointOfUnion — Mathlib

English

The union of all blocks across all j in J equals the union of J itself: the blocks cover exactly ∪J.

Русский

Объединение всех блоков по всем j из J равно объединению самого J.

LaTeX

$$$\bigcup\_{x\in J} \bigcup\_{A\in h_C.disjointOfUnion(h_J, x)} A = \bigcup\_{j\in J} j.$$$

Lean4

theorem sUnion_disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
    ⋃₀ ⋃ x ∈ J, (hC.disjointOfUnion hJ x : Set (Set α)) = ⋃₀ J :=
  (Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.2.2.2.symm

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