Theorems · Theorem · general topology

PolishSpace.exists_polishSpace_forall_le

∀ {α : Type u_1} {ι : Type u_3} [Countable ι] [t : TopologicalSpace α] [p : PolishSpace α] (m : ι → TopologicalSpace α),
  (∀ (n : ι), m n ≤ t) → (∀ (n : ι), PolishSpace α) → ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α

Given a Polish space, and countably many finer Polish topologies, there exists another Polish topology which is finer than all of them.

Defined in

Mathlib.Topology.MetricSpace.Polish

Cited by

2 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableTopologicalSpacePolishSpace