eq_of_eq_union_iUnion — Mathlib

English

Let I, J be families of subsets of cells. If D ∪ ⋃ (n) (j ∈ I n) openCell n j = D ∪ ⋃ (n) (j ∈ J n) openCell n j, then I = J.

Русский

Пусть I, J — семейства подмножеств клеток. Если D ∪ ⋃_{n} ⋃_{j∈I n} openCell n j = D ∪ ⋃_{n} ⋃_{j∈J n} openCell n j, то I = J.

LaTeX

$$$\Big(D \cup \bigcup_{n\in\mathbb{N}}\;\bigcup_{j\in I n}\ openCell (C := C) n j\Big) = \Big(D \cup \bigcup_{n\in\mathbb{N}}\;\bigcup_{j\in J n}\ openCell (C := C) n j\Big) \Rightarrow I = J$$$

Lean4

theorem eq_of_eq_union_iUnion [RelCWComplex C D] (I J : Π n, Set (cell C n))
    (hIJ : D ∪ ⋃ (n : ℕ) (j : I n), openCell (C := C) n j = D ∪ ⋃ (n : ℕ) (j : J n), openCell (C := C) n j) : I = J :=
  by
  ext n x
  exact ⟨fun h ↦ subset_of_eq_union_iUnion I J hIJ n h, fun h ↦ subset_of_eq_union_iUnion J I hIJ.symm n h⟩

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