Lean4
/-- The **measurable Schröder-Bernstein Theorem**: given measurable embeddings
`α → β` and `β → α`, we can find a measurable equivalence `α ≃ᵐ β`. -/
noncomputable def schroederBernstein {f : α → β} {g : β → α} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) :
α ≃ᵐ β :=
by
let F : Set α → Set α := fun A =>
(g '' (f '' A)ᶜ)ᶜ
-- We follow the proof of the usual SB theorem in mathlib,
-- the crux of which is finding a fixed point of this F.
-- However, we must find this fixed point manually instead of invoking Knaster-Tarski
-- in order to make sure it is measurable.
suffices Σ' A : Set α, MeasurableSet A ∧ F A = A by
classical
rcases this with ⟨A, Ameas, Afp⟩
let B := f '' A
have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
refine (MeasurableEquiv.sumCompl Ameas).symm.trans (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
apply MeasurableEquiv.sumCongr (hf.equivImage _)
have : Aᶜ = g '' Bᶜ := by
apply compl_injective
rw [← Afp]
simp [F, B]
rw [this]
exact (hg.equivImage _).symm
have Fmono : ∀ {A B}, A ⊆ B → F A ⊆ F B := fun h =>
compl_subset_compl.mpr <| Set.image_mono <| compl_subset_compl.mpr <| Set.image_mono h
let X : ℕ → Set α := fun n => F^[n] univ
refine ⟨iInter X, ?_, ?_⟩
· refine MeasurableSet.iInter fun n ↦ ?_
induction n with
| zero => exact MeasurableSet.univ
| succ n ih =>
rw [Function.iterate_succ', Function.comp_apply]
exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl
apply subset_antisymm
· apply subset_iInter
intro n
cases n
· exact subset_univ _
rw [Function.iterate_succ', Function.comp_apply]
exact Fmono (iInter_subset _ _)
rintro x hx ⟨y, hy, rfl⟩
rw [mem_iInter] at hx
apply hy
rw [hf.injective.injOn.image_iInter_eq]
rw [mem_iInter]
intro n
specialize hx n.succ
rw [Function.iterate_succ', Function.comp_apply] at hx
by_contra h
apply hx
exact ⟨y, h, rfl⟩
