instSecondCountableTopologyOfCompactSpaceOfMetrizableSpace

English

If X is compact and metrizable, then X is second countable.

Русский

Если X компактно и метризуемо, то X является второй счетной.

LaTeX

$$$[\text{CompactSpace } X] \land [\text{MetrizableSpace } X] \Rightarrow [\text{SecondCountableTopology } X]$$$

Lean4

instance (X : Type*) [TopologicalSpace X] [c : CompactSpace X] [MetrizableSpace X] : SecondCountableTopology X :=
  by
  obtain ⟨_, h⟩ := MetrizableSpace.exists_metric (X := X)
  rw [← h] at c ⊢
  infer_instance

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