English
Given a Polish space α and a family m(n) of topologies with m(n) ≤ t, there exists t′ with t′ ≤ m(n) for all n and t′ ≤ t, and t′ is Polish.
Русский
Для полиш-пространства α и семейства топологий m(n) с m(n) ≤ t существует t′, такое что t′ ≤ m(n) для всех n и t′ ≤ t, и t′ — полиш.
LaTeX
$$$$\\\\exists t': TopologicalSpace α, \\\\forall n, t' \\\\le m n \\\\land t' \\\\le t \\\\land @PolishSpace α t'.$$$$
Lean4
/-- Given a Polish space, and countably many finer Polish topologies, there exists another Polish
topology which is finer than all of them. -/
theorem exists_polishSpace_forall_le {ι : Type*} [Countable ι] [t : TopologicalSpace α] [p : PolishSpace α]
(m : ι → TopologicalSpace α) (hm : ∀ n, m n ≤ t) (h'm : ∀ n, @PolishSpace α (m n)) :
∃ t' : TopologicalSpace α, (∀ n, t' ≤ m n) ∧ t' ≤ t ∧ @PolishSpace α t' :=
⟨⨅ i : Option ι, i.elim t m, fun i ↦ iInf_le _ (some i), iInf_le _ none,
.iInf ⟨none, Option.forall.2 ⟨le_rfl, hm⟩⟩ <| Option.forall.2 ⟨p, h'm⟩⟩
