closed — Mathlib

English

If two families I, J of cells have the same union of open cells, then I = J.

Русский

Если два семейства клеток I и J имеют одинаковое объединение открытых клеток, то I = J.

LaTeX

$$$\forall I J : (n \mapsto Set (cell C n)),\; (\bigcup (n) (j : I n), openCell n j) = (\bigcup (n) (j : J n), openCell n j) \Rightarrow I = J$$$

Lean4

theorem closed (C : Set X) {D : Set X} [RelCWComplex C D] [T2Space X] (A : Set X) (asubc : A ⊆ C) :
    IsClosed A ↔ (∀ n (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D) :=
  by
  refine ⟨?_, closed' A asubc⟩
  exact fun closedA ↦ ⟨fun _ _ ↦ closedA.inter isClosed_closedCell, closedA.inter (isClosedBase C)⟩

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