eq_of_eq_union_iUnion — Mathlib

English

Let I, J be families as in RelCWComplex; if the unions of open cells over I and J are equal (without the base D), then I = J.

Русский

Пусть I, J — семейства клеток CW-комплекса; если объединения открытых клеток по I и по J совпадают, то I = J.

LaTeX

$$$\Big(\bigcup_{n\in\mathbb{N}}\;\bigcup_{j\in I n}\ openCell (C := C) n j\Big) = \Big(\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 [CWComplex C] (I J : Π n, Set (cell C n))
    (hIJ : ⋃ (n : ℕ) (j : I n), openCell (C := C) n j = ⋃ (n : ℕ) (j : J n), openCell (C := C) n j) : I = J :=
  by
  apply RelCWComplex.eq_of_eq_union_iUnion
  simp_rw [empty_union, hIJ]

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