English
If one Polish topology on a type refines another, they have the same Borel sets.
Русский
Если одна полиш‑топология на типе уточняет другую, их борелевы множества совпадают.
LaTeX
$$$\\text{borel}_t = \\text{borel}_{t'}$ when $t \\le t'$ and both are Polish.$$
Lean4
/-- If one Polish topology on a type refines another, they have the same Borel sets. -/
theorem borel_eq_borel_of_le {t t' : TopologicalSpace γ} (ht : PolishSpace (h := t)) (ht' : PolishSpace (h := t'))
(hle : t ≤ t') : @borel _ t = @borel _ t' :=
by
refine le_antisymm ?_ (borel_anti hle)
intro s hs
have e :=
@Continuous.measurableEmbedding _ _ (@borel _ t') t' _ _ (@BorelSpace.mk _ _ (borel γ) rfl) t _ (@borel _ t)
(@BorelSpace.mk _ t (@borel _ t) rfl) (continuous_id_of_le hle) injective_id
convert e.measurableSet_image.2 hs
simp only [id_eq, image_id']
