Measurable embeddings and equivalences

A measurable equivalence between measurable spaces is an equivalence which respects the σ-algebras, that is, for which both directions of the equivalence are measurable functions.

Main definitions

• MeasurableEmbedding: a map f : α → β is called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets.
• MeasurableEquiv: an equivalence α ≃ β is a measurable equivalence if its forward and inverse functions are measurable.

We prove a multitude of elementary lemmas about these, and one more substantial theorem:

• MeasurableEmbedding.schroederBernstein: the measurable Schröder-Bernstein Theorem: given measurable embeddings α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.

Notation

• We write α ≃ᵐ β for measurable equivalences between the measurable spaces α and β. This should not be confused with ≃ₘ which is used for diffeomorphisms between manifolds.

Tags

measurable equivalence, measurable embedding

structure MeasurableEmbedding {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop

A map f : α → β is called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable inverse g : Set.range f → α”, see MeasurableEmbedding.measurable_rangeSplitting, MeasurableEmbedding.of_measurable_inverse_range, and MeasurableEmbedding.of_measurable_inverse.

One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its range and the range is a measurable set. One implication is formalized as MeasurableEmbedding.equivRange; the other one follows from MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.subtype_coe, and MeasurableEmbedding.comp.

• injective : Function.Injective f

  A measurable embedding is injective.

• measurable : Measurable f

  A measurable embedding is a measurable function.

• measurableSet_image' ⦃s : Set α⦄ : MeasurableSet s → MeasurableSet (Set.image f s)

  The image of a measurable set under a measurable embedding is a measurable set.

theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) : Iff (MeasurableSet (Set.image f s)) (MeasurableSet s)

theorem MeasurableEmbedding.id {α : Type u_1} {mα : MeasurableSpace α} : MeasurableEmbedding _root_.id

theorem MeasurableEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {g : β → γ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) : MeasurableEmbedding (Function.comp g f)

theorem MeasurableEmbedding.subtype_coe {α : Type u_1} {s : Set α} {mα : MeasurableSpace α} (hs : MeasurableSet s) : MeasurableEmbedding Subtype.val

theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) : MeasurableSet (Set.range f)

theorem MeasurableEmbedding.measurableSet_preimage {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) {s : Set β} : Iff (MeasurableSet (Set.preimage f s)) (MeasurableSet (Inter.inter s (Set.range f)))

theorem MeasurableEmbedding.measurable_rangeSplitting {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) : Measurable (Set.rangeSplitting f)

theorem MeasurableEmbedding.measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} (hf : MeasurableEmbedding f) {g : α → γ} {g' : β → γ} (hg : Measurable g) (hg' : Measurable g') : Measurable (Function.extend f g g')

theorem MeasurableEmbedding.exists_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} (hf : MeasurableEmbedding f) {g : α → γ} (hg : Measurable g) (hne : β → Nonempty γ) : Exists fun (g' : β → γ) => And (Measurable g') (Eq (Function.comp g' f) g)

theorem MeasurableEmbedding.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {g : β → γ} (hg : MeasurableEmbedding g) : Iff (Measurable (Function.comp g f)) (Measurable f)

theorem MeasurableSet.of_union_range_cover {α : Type u_1} {α₁ : Type u_6} {α₂ : Type u_7} {mα : MeasurableSpace α} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {i₁ : α₁ → α} {i₂ : α₂ → α} {s : Set α} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (h : HasSubset.Subset Set.univ (Union.union (Set.range i₁) (Set.range i₂))) (hs₁ : MeasurableSet (Set.preimage i₁ s)) (hs₂ : MeasurableSet (Set.preimage i₂ s)) : MeasurableSet s

theorem MeasurableSet.of_union₃_range_cover {α : Type u_1} {α₁ : Type u_6} {α₂ : Type u_7} {α₃ : Type u_8} {mα : MeasurableSpace α} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {mα₃ : MeasurableSpace α₃} {i₁ : α₁ → α} {i₂ : α₂ → α} {i₃ : α₃ → α} {s : Set α} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (hi₃ : MeasurableEmbedding i₃) (h : HasSubset.Subset Set.univ (Union.union (Union.union (Set.range i₁) (Set.range i₂)) (Set.range i₃))) (hs₁ : MeasurableSet (Set.preimage i₁ s)) (hs₂ : MeasurableSet (Set.preimage i₂ s)) (hs₃ : MeasurableSet (Set.preimage i₃ s)) : MeasurableSet s

theorem Measurable.of_union_range_cover {α : Type u_1} {β : Type u_2} {α₁ : Type u_6} {α₂ : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {i₁ : α₁ → α} {i₂ : α₂ → α} {f : α → β} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (h : HasSubset.Subset Set.univ (Union.union (Set.range i₁) (Set.range i₂))) (hf₁ : Measurable (Function.comp f i₁)) (hf₂ : Measurable (Function.comp f i₂)) : Measurable f

theorem Measurable.of_union₃_range_cover {α : Type u_1} {β : Type u_2} {α₁ : Type u_6} {α₂ : Type u_7} {α₃ : Type u_8} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {mα₃ : MeasurableSpace α₃} {i₁ : α₁ → α} {i₂ : α₂ → α} {i₃ : α₃ → α} {f : α → β} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (hi₃ : MeasurableEmbedding i₃) (h : HasSubset.Subset Set.univ (Union.union (Union.union (Set.range i₁) (Set.range i₂)) (Set.range i₃))) (hf₁ : Measurable (Function.comp f i₁)) (hf₂ : Measurable (Function.comp f i₂)) (hf₃ : Measurable (Function.comp f i₃)) : Measurable f

theorem MeasurableSet.exists_measurable_proj {α : Type u_1} {s : Set α} {x✝ : MeasurableSpace α} (hs : MeasurableSet s) (hne : s.Nonempty) : Exists fun (f : α → s.Elem) => And (Measurable f) (∀ (x : s.Elem), Eq (f x.val) x)

structure MeasurableEquiv (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] extends Equiv α β : Type (max u_6 u_7)

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• measurable_toFun : Measurable (DFunLike.coe self.toEquiv)

  The forward function of a measurable equivalence is measurable.

• measurable_invFun : Measurable (DFunLike.coe self.symm)

  The inverse function of a measurable equivalence is measurable.

def «term_≃ᵐ_» : Lean.TrailingParserDescr

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

Equations

• Eq «term_≃ᵐ_» (Lean.ParserDescr.trailingNode `«term_≃ᵐ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵐ ") (Lean.ParserDescr.cat `term 26)))

theorem MeasurableEquiv.toEquiv_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : Function.Injective toEquiv

def MeasurableEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : EquivLike (MeasurableEquiv α β) α β

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableEquiv.coe_toEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (DFunLike.coe e.toEquiv) (DFunLike.coe e)

theorem MeasurableEquiv.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Measurable (DFunLike.coe e)

theorem MeasurableEquiv.coe_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : Equiv α β) (h1 : Measurable (DFunLike.coe e)) (h2 : Measurable (DFunLike.coe e.symm)) : Eq (DFunLike.coe { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }) (DFunLike.coe e)

def MeasurableEquiv.refl (α : Type u_6) [MeasurableSpace α] : MeasurableEquiv α α

Any measurable space is equivalent to itself.

Equations

• Eq (MeasurableEquiv.refl α) { toEquiv := Equiv.refl α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.instInhabited {α : Type u_1} [MeasurableSpace α] : Inhabited (MeasurableEquiv α α)

Equations

• Eq MeasurableEquiv.instInhabited { default := MeasurableEquiv.refl α }

def MeasurableEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) : MeasurableEquiv α γ

The composition of equivalences between measurable spaces.

Equations

• Eq (ab.trans bc) { toEquiv := ab.trans bc.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) : Eq (DFunLike.coe (ab.trans bc)) (Function.comp (DFunLike.coe bc) (DFunLike.coe ab))

def MeasurableEquiv.symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ab : MeasurableEquiv α β) : MeasurableEquiv β α

The inverse of an equivalence between measurable spaces.

Equations

• Eq ab.symm { toEquiv := ab.symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.coe_toEquiv_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (DFunLike.coe e.symm) (DFunLike.coe e.symm)

def MeasurableEquiv.Simps.apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : MeasurableEquiv α β) : α → β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

• Eq (MeasurableEquiv.Simps.apply h) (DFunLike.coe h)

def MeasurableEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : MeasurableEquiv α β) : β → α

See Note [custom simps projection]

Equations

• Eq (MeasurableEquiv.Simps.symm_apply h) (DFunLike.coe h.symm)

theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : MeasurableEquiv α β} (h : Eq (DFunLike.coe e₁) (DFunLike.coe e₂)) : Eq e₁ e₂

theorem MeasurableEquiv.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : MeasurableEquiv α β} : Iff (Eq e₁ e₂) (Eq (DFunLike.coe e₁) (DFunLike.coe e₂))

theorem MeasurableEquiv.symm_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : Equiv α β) (h1 : Measurable (DFunLike.coe e)) (h2 : Measurable (DFunLike.coe e.symm)) : Eq { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }

theorem MeasurableEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) (a✝ : α) : Eq (DFunLike.coe (ab.trans bc) a✝) (DFunLike.coe bc (DFunLike.coe ab a✝))

theorem MeasurableEquiv.refl_toEquiv (α : Type u_6) [MeasurableSpace α] : Eq (refl α).toEquiv (Equiv.refl α)

theorem MeasurableEquiv.refl_apply (α : Type u_6) [MeasurableSpace α] (a : α) : Eq (DFunLike.coe (refl α) a) a

theorem MeasurableEquiv.trans_toEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) : Eq (ab.trans bc).toEquiv (ab.trans bc.toEquiv)

theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq e.symm.symm e

theorem MeasurableEquiv.symm_bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : Function.Bijective symm

theorem MeasurableEquiv.symm_refl (α : Type u_6) [MeasurableSpace α] : Eq (refl α).symm (refl α)

theorem MeasurableEquiv.symm_comp_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (Function.comp (DFunLike.coe e.symm) (DFunLike.coe e)) id

theorem MeasurableEquiv.self_comp_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (Function.comp (DFunLike.coe e) (DFunLike.coe e.symm)) id

theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (y : β) : Eq (DFunLike.coe e (DFunLike.coe e.symm y)) y

theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (x : α) : Eq (DFunLike.coe e.symm (DFunLike.coe e x)) x

theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (e.symm.trans e) (refl β)

theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (e.trans e.symm) (refl α)

theorem MeasurableEquiv.surjective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Function.Surjective (DFunLike.coe e)

theorem MeasurableEquiv.bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Function.Bijective (DFunLike.coe e)

theorem MeasurableEquiv.injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Function.Injective (DFunLike.coe e)

theorem MeasurableEquiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set β) : Eq (Set.preimage (DFunLike.coe e.symm) (Set.preimage (DFunLike.coe e) s)) s

theorem MeasurableEquiv.image_eq_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set α) : Eq (Set.image (DFunLike.coe e) s) (Set.preimage (DFunLike.coe e.symm) s)

theorem MeasurableEquiv.preimage_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set α) : Eq (Set.preimage (DFunLike.coe e.symm) s) (Set.image (DFunLike.coe e) s)

theorem MeasurableEquiv.image_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set β) : Eq (Set.image (DFunLike.coe e.symm) s) (Set.preimage (DFunLike.coe e) s)

theorem MeasurableEquiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set β) (t : Set α) : Iff (Eq s (Set.image (DFunLike.coe e) t)) (Eq (Set.image (DFunLike.coe e.symm) s) t)

theorem MeasurableEquiv.image_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set β) : Eq (Set.image (DFunLike.coe e) (Set.preimage (DFunLike.coe e) s)) s

theorem MeasurableEquiv.preimage_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set α) : Eq (Set.preimage (DFunLike.coe e) (Set.image (DFunLike.coe e) s)) s

theorem MeasurableEquiv.measurableSet_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) {s : Set β} : Iff (MeasurableSet (Set.preimage (DFunLike.coe e) s)) (MeasurableSet s)

theorem MeasurableEquiv.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Iff (MeasurableSet (Set.image (DFunLike.coe e) s)) (MeasurableSet s)

theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : Eq (MeasurableSpace.map (DFunLike.coe e) inst✝) inst✝¹

theorem MeasurableEquiv.measurableEmbedding {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) : MeasurableEmbedding (DFunLike.coe e)

A measurable equivalence is a measurable embedding.

def MeasurableEquiv.cast {α β : Type u_6} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace β] (h : Eq α β) (hi : HEq i₁ i₂) : MeasurableEquiv α β

Equal measurable spaces are equivalent.

Equations

• Eq (MeasurableEquiv.cast h hi) { toEquiv := Equiv.cast h, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.ulift {α : Type u} [MeasurableSpace α] : MeasurableEquiv (ULift α) α

Measurable equivalence between ULift α and α.

Equations

• Eq MeasurableEquiv.ulift { toEquiv := Equiv.ulift, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : β → γ} (e : MeasurableEquiv α β) : Iff (Measurable (Function.comp f (DFunLike.coe e))) (Measurable f)

def MeasurableEquiv.ofUniqueOfUnique (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] [Unique α] [Unique β] : MeasurableEquiv α β

Any two types with unique elements are measurably equivalent.

Equations

• Eq (MeasurableEquiv.ofUniqueOfUnique α β) { toEquiv := Equiv.ofUnique α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : MeasurableEquiv α β) (cd : MeasurableEquiv γ δ) : MeasurableEquiv (Prod α γ) (Prod β δ)

Products of equivalent measurable spaces are equivalent.

Equations

• Eq (ab.prodCongr cd) { toEquiv := ab.prodCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.prodComm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : MeasurableEquiv (Prod α β) (Prod β α)

Products of measurable spaces are symmetric.

Equations

• Eq MeasurableEquiv.prodComm { toEquiv := Equiv.prodComm α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] : MeasurableEquiv (Prod (Prod α β) γ) (Prod α (Prod β γ))

Products of measurable spaces are associative.

Equations

• Eq MeasurableEquiv.prodAssoc { toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.punitProd {α : Type u_1} [MeasurableSpace α] : MeasurableEquiv (Prod PUnit α) α

PUnit is a left identity for product of measurable spaces up to a measurable equivalence.

Equations

• Eq MeasurableEquiv.punitProd { toEquiv := Equiv.punitProd α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.prodPUnit {α : Type u_1} [MeasurableSpace α] : MeasurableEquiv (Prod α PUnit) α

PUnit is a right identity for product of measurable spaces up to a measurable equivalence.

Equations

• Eq MeasurableEquiv.prodPUnit { toEquiv := Equiv.prodPUnit α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : MeasurableEquiv α β) (cd : MeasurableEquiv γ δ) : MeasurableEquiv (Sum α γ) (Sum β δ)

Sums of measurable spaces are symmetric.

Equations

• Eq (ab.sumCongr cd) { toEquiv := ab.sumCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.Set.prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (s : Set α) (t : Set β) : MeasurableEquiv (SProd.sprod s t).Elem (Prod s.Elem t.Elem)

s ×ˢ t ≃ (s × t) as measurable spaces.

Equations

• Eq (MeasurableEquiv.Set.prod s t) { toEquiv := Equiv.Set.prod s t, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.Set.univ (α : Type u_6) [MeasurableSpace α] : MeasurableEquiv _root_.Set.univ.Elem α

univ α ≃ α as measurable spaces.

Equations

• Eq (MeasurableEquiv.Set.univ α) { toEquiv := Equiv.Set.univ α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.Set.singleton {α : Type u_1} [MeasurableSpace α] (a : α) : MeasurableEquiv (Singleton.singleton a).Elem Unit

{a} ≃ Unit as measurable spaces.

Equations

• Eq (MeasurableEquiv.Set.singleton a) { toEquiv := Equiv.Set.singleton a, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.Set.rangeInl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : MeasurableEquiv (Set.range Sum.inl).Elem α

α is equivalent to its image in α ⊕ β as measurable spaces.

Equations

• Eq MeasurableEquiv.Set.rangeInl { toEquiv := Equiv.Set.rangeInl α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.Set.rangeInr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : MeasurableEquiv (Set.range Sum.inr).Elem β

β is equivalent to its image in α ⊕ β as measurable spaces.

Equations

• Eq MeasurableEquiv.Set.rangeInr { toEquiv := Equiv.Set.rangeInr α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.sumProdDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] : MeasurableEquiv (Prod (Sum α β) γ) (Sum (Prod α γ) (Prod β γ))

Products distribute over sums (on the right) as measurable spaces.

Equations

• Eq (MeasurableEquiv.sumProdDistrib α β γ) { toEquiv := Equiv.sumProdDistrib α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.prodSumDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] : MeasurableEquiv (Prod α (Sum β γ)) (Sum (Prod α β) (Prod α γ))

Products distribute over sums (on the left) as measurable spaces.

Equations

• Eq (MeasurableEquiv.prodSumDistrib α β γ) (MeasurableEquiv.prodComm.trans ((MeasurableEquiv.sumProdDistrib β γ α).trans (MeasurableEquiv.prodComm.sumCongr MeasurableEquiv.prodComm)))

def MeasurableEquiv.sumProdSum (α : Type u_6) (β : Type u_7) (γ : Type u_8) (δ : Type u_9) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] : MeasurableEquiv (Prod (Sum α β) (Sum γ δ)) (Sum (Sum (Prod α γ) (Prod α δ)) (Sum (Prod β γ) (Prod β δ)))

Products distribute over sums as measurable spaces.

Equations

• Eq (MeasurableEquiv.sumProdSum α β γ δ) ((MeasurableEquiv.sumProdDistrib α β (Sum γ δ)).trans ((MeasurableEquiv.prodSumDistrib α γ δ).sumCongr (MeasurableEquiv.prodSumDistrib β γ δ)))

def MeasurableEquiv.piCongrRight {δ' : Type u_5} {π : δ' → Type u_6} {π' : δ' → Type u_7} [(x : δ') → MeasurableSpace (π x)] [(x : δ') → MeasurableSpace (π' x)] (e : (a : δ') → MeasurableEquiv (π a) (π' a)) : MeasurableEquiv ((a : δ') → π a) ((a : δ') → π' a)

A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence between Π a, β₁ a and Π a, β₂ a.

Equations

• Eq (MeasurableEquiv.piCongrRight e) { toEquiv := Equiv.piCongrRight fun (a : δ') => (e a).toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.piCongrLeft {δ : Type u_4} {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (f : Equiv δ δ') : MeasurableEquiv ((b : δ) → π (DFunLike.coe f b)) ((a : δ') → π a)

Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.

Equations

• Eq (MeasurableEquiv.piCongrLeft π f) { toEquiv := Equiv.piCongrLeft π f, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : Equiv δ δ') : Eq (DFunLike.coe (piCongrLeft π f)) (DFunLike.coe (Equiv.piCongrLeft π f))

theorem MeasurableEquiv.piCongrLeft_apply_apply {ι : Type u_8} {ι' : Type u_9} (e : Equiv ι ι') {β : ι' → Type u_10} [(i' : ι') → MeasurableSpace (β i')] (x : (i : ι) → β (DFunLike.coe e i)) (i : ι) : Eq (DFunLike.coe (piCongrLeft (fun (i' : ι') => β i') e) x (DFunLike.coe e i)) (x i)

def MeasurableEquiv.arrowProdEquivProdArrow (α : Type u_8) (β : Type u_9) (γ : Type u_10) [MeasurableSpace α] [MeasurableSpace β] : MeasurableEquiv (γ → Prod α β) (Prod (γ → α) (γ → β))

The isomorphism (γ → α × β) ≃ (γ → α) × (γ → β) as a measurable equivalence.

Equations

• Eq (MeasurableEquiv.arrowProdEquivProdArrow α β γ) { toEquiv := Equiv.arrowProdEquivProdArrow γ (fun (i : γ) => α) fun (i : γ) => β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.arrowCongr' {α₁ : Type u_8} {β₁ : Type u_9} {α₂ : Type u_10} {β₂ : Type u_11} [MeasurableSpace β₁] [MeasurableSpace β₂] (hα : Equiv α₁ α₂) (hβ : MeasurableEquiv β₁ β₂) : MeasurableEquiv (α₁ → β₁) (α₂ → β₂)

The measurable equivalence (α₁ → β₁) ≃ᵐ (α₂ → β₂) induced by α₁ ≃ α₂ and β₁ ≃ᵐ β₂.

Equations

• Eq (MeasurableEquiv.arrowCongr' hα hβ) { toEquiv := hα.arrowCongr' (EquivLike.toEquiv hβ), measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.piMeasurableEquivTProd {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), Membership.mem l i) : MeasurableEquiv ((i : δ') → π i) (List.TProd π l)

Pi-types are measurably equivalent to iterated products.

Equations

• Eq (MeasurableEquiv.piMeasurableEquivTProd hnd h) { toEquiv := List.TProd.piEquivTProd hnd h, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.piMeasurableEquivTProd_apply {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), Membership.mem l i) : Eq (DFunLike.coe (piMeasurableEquivTProd hnd h)) (List.TProd.mk l)

theorem MeasurableEquiv.piMeasurableEquivTProd_symm_apply {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), Membership.mem l i) : Eq (DFunLike.coe (piMeasurableEquivTProd hnd h).symm) (List.TProd.elim' h)

def MeasurableEquiv.piUnique {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] : MeasurableEquiv ((i : δ') → π i) (π Inhabited.default)

The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆ when the domain of π only contains ⋆

Equations

• Eq (MeasurableEquiv.piUnique π) { toEquiv := Equiv.piUnique π, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] : Eq (DFunLike.coe (piUnique π)) fun (f : (i : δ') → π i) => f Inhabited.default

theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] : Eq (DFunLike.coe (piUnique π).symm) uniqueElim

def MeasurableEquiv.funUnique (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] : MeasurableEquiv (α → β) β

If α has a unique term, then the type of function α → β is measurably equivalent to β.

Equations

• Eq (MeasurableEquiv.funUnique α β) (MeasurableEquiv.piUnique fun (a : α) => β)

theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] : Eq (DFunLike.coe (funUnique α β)) fun (f : α → β) => f Inhabited.default

theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] : Eq (DFunLike.coe (funUnique α β).symm) uniqueElim

def MeasurableEquiv.piFinTwo (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] : MeasurableEquiv ((i : Fin 2) → α i) (Prod (α 0) (α 1))

The space Π i : Fin 2, α i is measurably equivalent to α 0 × α 1.

Equations

• Eq (MeasurableEquiv.piFinTwo α) { toEquiv := piFinTwoEquiv α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.piFinTwo_apply (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] : Eq (DFunLike.coe (piFinTwo α)) fun (f : (i : Fin 2) → α i) => { fst := f 0, snd := f 1 }

theorem MeasurableEquiv.piFinTwo_symm_apply (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] : Eq (DFunLike.coe (piFinTwo α).symm) fun (p : Prod (α 0) (α 1)) => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

def MeasurableEquiv.finTwoArrow {α : Type u_1} [MeasurableSpace α] : MeasurableEquiv (Fin 2 → α) (Prod α α)

The space Fin 2 → α is measurably equivalent to α × α.

Equations

• Eq MeasurableEquiv.finTwoArrow (MeasurableEquiv.piFinTwo fun (x : Fin 2) => α)

theorem MeasurableEquiv.finTwoArrow_symm_apply {α : Type u_1} [MeasurableSpace α] : Eq (DFunLike.coe finTwoArrow.symm) fun (p : Prod α α) => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [MeasurableSpace α] : Eq (DFunLike.coe finTwoArrow) fun (f : Fin 2 → α) => { fst := f 0, snd := f 1 }

def MeasurableEquiv.piFinSuccAbove {n : Nat} (α : Fin (HAdd.hAdd n 1) → Type u_8) [(i : Fin (HAdd.hAdd n 1)) → MeasurableSpace (α i)] (i : Fin (HAdd.hAdd n 1)) : MeasurableEquiv ((j : Fin (HAdd.hAdd n 1)) → α j) (Prod (α i) ((j : Fin n) → α (i.succAbove j)))

Measurable equivalence between Π j : Fin (n + 1), α j and α i × Π j : Fin n, α (Fin.succAbove i j).

Measurable version of Fin.insertNthEquiv.

Equations

• Eq (MeasurableEquiv.piFinSuccAbove α i) { toEquiv := (Fin.insertNthEquiv α i).symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.piFinSuccAbove_symm_apply {n : Nat} (α : Fin (HAdd.hAdd n 1) → Type u_8) [(i : Fin (HAdd.hAdd n 1)) → MeasurableSpace (α i)] (i : Fin (HAdd.hAdd n 1)) : Eq (DFunLike.coe (piFinSuccAbove α i).symm) (DFunLike.coe (Fin.insertNthEquiv α i))

theorem MeasurableEquiv.piFinSuccAbove_apply {n : Nat} (α : Fin (HAdd.hAdd n 1) → Type u_8) [(i : Fin (HAdd.hAdd n 1)) → MeasurableSpace (α i)] (i : Fin (HAdd.hAdd n 1)) : Eq (DFunLike.coe (piFinSuccAbove α i)) (DFunLike.coe (Fin.insertNthEquiv α i).symm)

def MeasurableEquiv.piEquivPiSubtypeProd {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] : MeasurableEquiv ((i : δ') → π i) (Prod ((i : Subtype p) → π i.val) ((i : Subtype fun (i : δ') => Not (p i)) → π i.val))

Measurable equivalence between (dependent) functions on a type and pairs of functions on {i // p i} and {i // ¬p i}. See also Equiv.piEquivPiSubtypeProd.

Equations

• Eq (MeasurableEquiv.piEquivPiSubtypeProd π p) { toEquiv := Equiv.piEquivPiSubtypeProd p π, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.piEquivPiSubtypeProd_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] : Eq (DFunLike.coe (piEquivPiSubtypeProd π p)) fun (f : (i : δ') → π i) => { fst := fun (x : Subtype fun (x : δ') => p x) => f x.val, snd := fun (x : Subtype fun (x : δ') => Not (p x)) => f x.val }

theorem MeasurableEquiv.piEquivPiSubtypeProd_symm_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] : Eq (DFunLike.coe (piEquivPiSubtypeProd π p).symm) fun (f : Prod ((i : Subtype fun (x : δ') => p x) → π i.val) ((i : Subtype fun (x : δ') => Not (p x)) → π i.val)) (x : δ') => if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩

def MeasurableEquiv.sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : Sum δ δ' → Type u_8) [(i : Sum δ δ') → MeasurableSpace (α i)] : MeasurableEquiv ((i : Sum δ δ') → α i) (Prod ((i : δ) → α (Sum.inl i)) ((i' : δ') → α (Sum.inr i')))

The measurable equivalence between the pi type over a sum type and a product of pi-types. This is similar to MeasurableEquiv.piEquivPiSubtypeProd.

Equations

• Eq (MeasurableEquiv.sumPiEquivProdPi α) { toEquiv := Equiv.sumPiEquivProdPi α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : Sum δ δ' → Type u_8) [(i : Sum δ δ') → MeasurableSpace (α i)] : Eq (DFunLike.coe (sumPiEquivProdPi α)) (DFunLike.coe (Equiv.sumPiEquivProdPi α))

theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : Sum δ δ' → Type u_8) [(i : Sum δ δ') → MeasurableSpace (α i)] : Eq (DFunLike.coe (sumPiEquivProdPi α).symm) (DFunLike.coe (Equiv.sumPiEquivProdPi α).symm)

def MeasurableEquiv.piOptionEquivProd {δ : Type u_8} (α : Option δ → Type u_9) [(i : Option δ) → MeasurableSpace (α i)] : MeasurableEquiv ((i : Option δ) → α i) (Prod ((i : δ) → α (Option.some i)) (α Option.none))

The measurable equivalence for (dependent) functions on an Option type (∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none.

Equations

• One or more equations did not get rendered due to their size.

def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) : MeasurableEquiv (Prod ((i : Subtype fun (x : δ') => Membership.mem s x) → π i.val) ((i : Subtype fun (x : δ') => Membership.mem t x) → π i.val)) ((i : Subtype fun (x : δ') => Membership.mem (Union.union s t) x) → π i.val)

The measurable equivalence (∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i) for disjoint finsets s and t. Equiv.piFinsetUnion as a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

def MeasurableEquiv.sumCompl {α : Type u_1} [MeasurableSpace α] {s : Set α} [DecidablePred fun (x : α) => Membership.mem s x] (hs : MeasurableSet s) : MeasurableEquiv (Sum s.Elem (HasCompl.compl s).Elem) α

If s is a measurable set in a measurable space, that space is equivalent to the sum of s and sᶜ.

Equations

• Eq (MeasurableEquiv.sumCompl hs) { toEquiv := Equiv.sumCompl fun (x : α) => Membership.mem s x, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.ofInvolutive {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) : MeasurableEquiv α α

Convert a measurable involutive function f to a measurable permutation with toFun = invFun = f. See also Function.Involutive.toPerm.

Equations

• Eq (MeasurableEquiv.ofInvolutive f hf hf') { toEquiv := Function.Involutive.toPerm f hf, measurable_toFun := hf', measurable_invFun := hf' }

theorem MeasurableEquiv.ofInvolutive_toEquiv {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) : Eq (ofInvolutive f hf hf').toEquiv (Function.Involutive.toPerm f hf)

theorem MeasurableEquiv.ofInvolutive_apply {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) (a : α) : Eq (DFunLike.coe (ofInvolutive f hf hf') a) (f a)

theorem MeasurableEquiv.ofInvolutive_symm {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) : Eq (ofInvolutive f hf hf').symm (ofInvolutive f hf hf')

theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) : Eq (MeasurableSpace.comap f inst✝) inst✝¹

theorem MeasurableEmbedding.iff_comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} : Iff (MeasurableEmbedding f) (And (Function.Injective f) (And (Eq (MeasurableSpace.comap f inst✝) inst✝¹) (MeasurableSet (Set.range f))))

noncomputable def MeasurableEmbedding.equivImage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (s : Set α) (hf : MeasurableEmbedding f) : MeasurableEquiv s.Elem (Set.image f s).Elem

A set is equivalent to its image under a function f as measurable spaces, if f is a measurable embedding

Equations

• Eq (MeasurableEmbedding.equivImage s hf) { toEquiv := Equiv.Set.image f s ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

noncomputable def MeasurableEmbedding.equivRange {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) : MeasurableEquiv α (Set.range f).Elem

The domain of f is equivalent to its range as measurable spaces, if f is a measurable embedding

Equations

• Eq hf.equivRange ((MeasurableEquiv.Set.univ α).symm.trans ((MeasurableEmbedding.equivImage Set.univ hf).trans (MeasurableEquiv.cast ⋯ ⋯)))

theorem MeasurableEmbedding.of_measurable_inverse_on_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : (Set.range f).Elem → α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g (Set.rangeFactorization f)) : MeasurableEmbedding f

theorem MeasurableEmbedding.of_measurable_inverse {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : β → α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g f) : MeasurableEmbedding f

noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : β → α} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) : MeasurableEquiv α β

The measurable Schröder-Bernstein Theorem: given measurable embeddings α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableSpace.comap_compl {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [BooleanAlgebra β] (h : Measurable HasCompl.compl) (f : α → β) : Eq (MeasurableSpace.comap (fun (a : α) => HasCompl.compl (f a)) inferInstance) (MeasurableSpace.comap f inferInstance)

theorem MeasurableSpace.comap_not {α : Type u_1} (p : α → Prop) : Eq (MeasurableSpace.comap (fun (a : α) => Not (p a)) inferInstance) (MeasurableSpace.comap p inferInstance)