instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace

English

If α is a TopologicalSpace with SeparableSpace and IsCompletelyMetrizableSpace, then α is Polish.

Русский

Если у α есть топологическое пространство, оно сепарируемо и полностью метризируемо, то α является PolishSpace.

LaTeX

$$$$\\\\forall α, [TopologicalSpace α], [TopologicalSpace.SeparableSpace α], [TopologicalSpace.IsCompletelyMetrizableSpace α] \\\\Rightarrow PolishSpace α.$$$$

Lean4

instance [TopologicalSpace α] [SeparableSpace α] [IsCompletelyMetrizableSpace α] : PolishSpace α :=
  by
  letI := upgradeIsCompletelyMetrizable α
  haveI := UniformSpace.secondCountable_of_separable α
  constructor

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