cellFrontier_subset_complex — Mathlib

English

For CWComplex C, if the unions of open cells over I and J are equal, then I = J.

Русский

Для CW-комплекса C, если объединения открытых клеток по I и J совпадают, то I = J.

LaTeX

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

Lean4

theorem cellFrontier_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ C :=
  (cellFrontier_subset_closedCell n j).trans (closedCell_subset_complex n j)

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