coclosedCompact_eq_cocompact — Mathlib

English

In an R1 space, the coclosedCompact filter equals the cocompact filter.

Русский

В R1-пространстве фильтры coclosedCompact и cocompact совпадают.

LaTeX

$$coclosedCompact X = cocompact X$$

Lean4

/-- In an R₁ space, the filters `coclosedCompact` and `cocompact` are equal. -/
@[simp]
theorem coclosedCompact_eq_cocompact : coclosedCompact X = cocompact X :=
  by
  refine le_antisymm ?_ cocompact_le_coclosedCompact
  rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]
  exact fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩

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