borelSchroederBernstein — Mathlib

English

There exists a measurable equivalence between any two uncountable standard Borel spaces.

Русский

Существует измеримое эквивалентное соответствие между любыми двумя несчётными стандартными пространствами Бореля.

LaTeX

$$MeasurableEquiv α β$$

Lean4

/-- If two standard Borel spaces admit Borel measurable injections to one another,
then they are Borel isomorphic. -/
noncomputable def borelSchroederBernstein {f : α → β} {g : β → α} (fmeas : Measurable f) (finj : Function.Injective f)
    (gmeas : Measurable g) (ginj : Function.Injective g) : α ≃ᵐ β :=
  letI := upgradeStandardBorel α
  letI := upgradeStandardBorel β
  (fmeas.measurableEmbedding finj).schroederBernstein (gmeas.measurableEmbedding ginj)

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