openCell_subset_complex — Mathlib

English

Equality of unions of open cells implies equality of identically indexed cell sets under RelCWComplex.

Русский

Собственные объединения открытых клеток равны тогда и только тогда, когда индексы клеток совпадают.

LaTeX

$$$\forall I J : (n \mapsto Set (cell C n)),\; (D \cup \bigcup_{n} \bigcup_{j \in I n} openCell n j) = (D \cup \bigcup_{n} \bigcup_{j \in J n} openCell n j) \Rightarrow I = J$$$

Lean4

theorem openCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ C :=
  (openCell_subset_closedCell _ _).trans (closedCell_subset_complex _ _)

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