of_compactlyCoherentSpace_of_t2 — Mathlib

English

A compactly coherent space that is Hausdorff is compactly generated.

Русский

Компактно-коhерентное пространство, являющееся хаусдорфовым, компактно-генерируемо.

LaTeX

$$[T2Space X] [CompactlyCoherentSpace X] \\Rightarrow \\text{CompactlyGeneratedSpace}(X)$$

Lean4

/-- A compactly coherent space that is Hausdorff is compactly generated. -/
instance of_compactlyCoherentSpace_of_t2 [T2Space X] [CompactlyCoherentSpace X] : CompactlyGeneratedSpace X :=
  by
  apply compactlyGeneratedSpace_of_isClosed_of_t2
  intro s hs
  rw [CompactlyCoherentSpace.isClosed_iff]
  intro K hK
  rw [← Subtype.preimage_coe_inter_self]
  exact (hs K hK).preimage_val

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