closed — Mathlib

English

For A ⊆ C, A is closed if and only if A ∩ closedCell n j is closed for all n and j, and A ∩ D is closed.

Русский

Для A ⊆ C: A замкнуто тогда и только тогда, когда A ∩ closedCell n j замкнуто для всех n и j, и A ∩ D замкнуто.

LaTeX

$$$\forall {X} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (A : Set X) (asubc : A ⊆ C) : IsClosed A \iff (\forall n (j : cell C n), IsClosed (A \cap closedCell n j)) \land IsClosed (A \cap D)$$

Lean4

theorem closed (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc : A ⊆ C) :
    IsClosed A ↔ ∀ n (j : cell C n), IsClosed (A ∩ closedCell n j) :=
  by
  have := RelCWComplex.closed C A asubc
  simp_all

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