isClosed — Mathlib

English

In a RelCWComplex, the base C is closed in a Hausdorff space if the space is T2.

Русский

В RelCWComplex база C замкнута в пространстве Х, если Х — T2.

LaTeX

$$$IsClosed\ C$$$

Lean4

theorem isClosed [T2Space X] [RelCWComplex C D] : IsClosed C :=
  by
  rw [closed C C (by rfl)]
  constructor
  · intros
    rw [inter_eq_right.2 (closedCell_subset_complex _ _)]
    exact isClosed_closedCell
  · rw [inter_eq_right.2 base_subset_complex]
    exact isClosedBase C

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