Documentation

Mathlib.MeasureTheory.MeasurableSpace.Embedding

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 #

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

Notation #

Tags #

measurable equivalence, measurable embedding

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

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 sMeasurableSet (f '' s)

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

Instances For
    theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
    theorem MeasurableEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {g : βγ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
    theorem MeasurableEmbedding.subtype_coe {α : Type u_1} {s : Set α} {mα : MeasurableSpace α} (hs : MeasurableSet s) :
    theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
    theorem MeasurableEmbedding.measurableSet_preimage {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) {s : Set β} :
    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') :
    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 γ) :
    ∃ (g' : βγ), Measurable g' 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) :
    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 : Set.univ Set.range i₁ Set.range i₂) (hs₁ : MeasurableSet (i₁ ⁻¹' s)) (hs₂ : MeasurableSet (i₂ ⁻¹' 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 : Set.univ Set.range i₁ Set.range i₂ Set.range i₃) (hs₁ : MeasurableSet (i₁ ⁻¹' s)) (hs₂ : MeasurableSet (i₂ ⁻¹' s)) (hs₃ : MeasurableSet (i₃ ⁻¹' 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 : Set.univ Set.range i₁ Set.range i₂) (hf₁ : Measurable (f i₁)) (hf₂ : Measurable (f i₂)) :
    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 : Set.univ Set.range i₁ Set.range i₂ Set.range i₃) (hf₁ : Measurable (f i₁)) (hf₂ : Measurable (f i₂)) (hf₃ : Measurable (f i₃)) :
    theorem MeasurableSet.exists_measurable_proj {α : Type u_1} {s : Set α} {x✝ : MeasurableSpace α} (hs : MeasurableSet s) (hne : s.Nonempty) :
    ∃ (f : αs), Measurable f ∀ (x : s), f x = x
    structure MeasurableEquiv (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] extends α β :
    Type (max u_6 u_7)

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

    Instances For

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

      Equations
      Instances For
        theorem MeasurableEquiv.toEquiv_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
        Function.Injective MeasurableEquiv.toEquiv
        instance MeasurableEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
        EquivLike (α ≃ᵐ β) α β
        Equations
        • MeasurableEquiv.instEquivLike = { coe := fun (e : α ≃ᵐ β) => e.toEquiv, inv := fun (e : α ≃ᵐ β) => e.symm, left_inv := , right_inv := , coe_injective' := }
        @[simp]
        theorem MeasurableEquiv.coe_toEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
        e.toEquiv = e
        theorem MeasurableEquiv.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
        @[simp]
        theorem MeasurableEquiv.coe_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α β) (h1 : Measurable e) (h2 : Measurable e.symm) :
        { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 } = e
        def MeasurableEquiv.refl (α : Type u_6) [MeasurableSpace α] :
        α ≃ᵐ α

        Any measurable space is equivalent to itself.

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

          The composition of equivalences between measurable spaces.

          Equations
          • ab.trans bc = { toEquiv := ab.trans bc.toEquiv, measurable_toFun := , measurable_invFun := }
          Instances For
            theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
            (ab.trans bc) = bc ab
            def MeasurableEquiv.symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ab : α ≃ᵐ β) :
            β ≃ᵐ α

            The inverse of an equivalence between measurable spaces.

            Equations
            • ab.symm = { toEquiv := ab.symm, measurable_toFun := , measurable_invFun := }
            Instances For
              @[simp]
              theorem MeasurableEquiv.coe_toEquiv_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
              e.symm = e.symm
              def MeasurableEquiv.Simps.apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : α ≃ᵐ β) :
              αβ

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

              Equations
              Instances For
                def MeasurableEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : α ≃ᵐ β) :
                βα

                See Note [custom simps projection]

                Equations
                Instances For
                  theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β} (h : e₁ = e₂) :
                  e₁ = e₂
                  @[simp]
                  theorem MeasurableEquiv.symm_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α β) (h1 : Measurable e) (h2 : Measurable e.symm) :
                  { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm = { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
                  @[simp]
                  theorem MeasurableEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) (a✝ : α) :
                  (ab.trans bc) a✝ = bc (ab a✝)
                  @[simp]
                  theorem MeasurableEquiv.refl_apply (α : Type u_6) [MeasurableSpace α] (a : α) :
                  @[simp]
                  theorem MeasurableEquiv.trans_toEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
                  (ab.trans bc).toEquiv = ab.trans bc.toEquiv
                  @[simp]
                  theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  e.symm.symm = e
                  theorem MeasurableEquiv.symm_bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                  Function.Bijective MeasurableEquiv.symm
                  @[simp]
                  theorem MeasurableEquiv.symm_comp_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  e.symm e = id
                  @[simp]
                  theorem MeasurableEquiv.self_comp_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  e e.symm = id
                  @[simp]
                  theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (y : β) :
                  e (e.symm y) = y
                  @[simp]
                  theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (x : α) :
                  e.symm (e x) = x
                  @[simp]
                  theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  e.symm.trans e = MeasurableEquiv.refl β
                  @[simp]
                  theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  e.trans e.symm = MeasurableEquiv.refl α
                  theorem MeasurableEquiv.surjective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  theorem MeasurableEquiv.bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  theorem MeasurableEquiv.injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  @[simp]
                  theorem MeasurableEquiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
                  e.symm ⁻¹' (e ⁻¹' s) = s
                  theorem MeasurableEquiv.image_eq_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
                  e '' s = e.symm ⁻¹' s
                  theorem MeasurableEquiv.preimage_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
                  e.symm ⁻¹' s = e '' s
                  theorem MeasurableEquiv.image_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
                  e.symm '' s = e ⁻¹' s
                  theorem MeasurableEquiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) (t : Set α) :
                  s = e '' t e.symm '' s = t
                  @[simp]
                  theorem MeasurableEquiv.image_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
                  e '' (e ⁻¹' s) = s
                  @[simp]
                  theorem MeasurableEquiv.preimage_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
                  e ⁻¹' (e '' s) = s
                  @[simp]
                  theorem MeasurableEquiv.measurableSet_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) {s : Set β} :
                  @[simp]
                  theorem MeasurableEquiv.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  @[simp]
                  theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                  MeasurableSpace.map (⇑e) inst✝ = inst✝¹

                  A measurable equivalence is a measurable embedding.

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

                  Equal measurable spaces are equivalent.

                  Equations
                  Instances For

                    Measurable equivalence between ULift α and α.

                    Equations
                    • MeasurableEquiv.ulift = { toEquiv := Equiv.ulift, measurable_toFun := , measurable_invFun := }
                    Instances For
                      theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : βγ} (e : α ≃ᵐ β) :
                      def MeasurableEquiv.ofUniqueOfUnique (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] [Unique α] [Unique β] :
                      α ≃ᵐ β

                      Any two types with unique elements are measurably equivalent.

                      Equations
                      Instances For
                        def MeasurableEquiv.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
                        α × γ ≃ᵐ β × δ

                        Products of equivalent measurable spaces are equivalent.

                        Equations
                        • ab.prodCongr cd = { toEquiv := ab.prodCongr cd.toEquiv, measurable_toFun := , measurable_invFun := }
                        Instances For
                          def MeasurableEquiv.prodComm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                          α × β ≃ᵐ β × α

                          Products of measurable spaces are symmetric.

                          Equations
                          • MeasurableEquiv.prodComm = { toEquiv := Equiv.prodComm α β, measurable_toFun := , measurable_invFun := }
                          Instances For
                            def MeasurableEquiv.prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                            (α × β) × γ ≃ᵐ α × β × γ

                            Products of measurable spaces are associative.

                            Equations
                            • MeasurableEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := , measurable_invFun := }
                            Instances For

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

                              Equations
                              • MeasurableEquiv.punitProd = { toEquiv := Equiv.punitProd α, measurable_toFun := , measurable_invFun := }
                              Instances For

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

                                Equations
                                • MeasurableEquiv.prodPUnit = { toEquiv := Equiv.prodPUnit α, measurable_toFun := , measurable_invFun := }
                                Instances For
                                  def MeasurableEquiv.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
                                  α γ ≃ᵐ β δ

                                  Sums of measurable spaces are symmetric.

                                  Equations
                                  • ab.sumCongr cd = { toEquiv := ab.sumCongr cd.toEquiv, measurable_toFun := , measurable_invFun := }
                                  Instances For
                                    def MeasurableEquiv.Set.prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (s : Set α) (t : Set β) :
                                    (s ×ˢ t) ≃ᵐ s × t

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

                                    Equations
                                    Instances For
                                      def MeasurableEquiv.Set.univ (α : Type u_6) [MeasurableSpace α] :
                                      Set.univ ≃ᵐ α

                                      univ α ≃ α as measurable spaces.

                                      Equations
                                      Instances For
                                        def MeasurableEquiv.Set.singleton {α : Type u_1} [MeasurableSpace α] (a : α) :
                                        {a} ≃ᵐ Unit

                                        {a} ≃ Unit as measurable spaces.

                                        Equations
                                        Instances For
                                          def MeasurableEquiv.Set.rangeInl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                                          (Set.range Sum.inl) ≃ᵐ α

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

                                          Equations
                                          • MeasurableEquiv.Set.rangeInl = { toEquiv := Equiv.Set.rangeInl α β, measurable_toFun := , measurable_invFun := }
                                          Instances For
                                            def MeasurableEquiv.Set.rangeInr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                                            (Set.range Sum.inr) ≃ᵐ β

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

                                            Equations
                                            • MeasurableEquiv.Set.rangeInr = { toEquiv := Equiv.Set.rangeInr α β, measurable_toFun := , measurable_invFun := }
                                            Instances For
                                              def MeasurableEquiv.sumProdDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                              (α β) × γ ≃ᵐ α × γ β × γ

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

                                              Equations
                                              Instances For
                                                def MeasurableEquiv.prodSumDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                                α × (β γ) ≃ᵐ α × β α × γ

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

                                                Equations
                                                Instances For
                                                  def MeasurableEquiv.sumProdSum (α : Type u_6) (β : Type u_7) (γ : Type u_8) (δ : Type u_9) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] :
                                                  (α β) × (γ δ) ≃ᵐ (α × γ α × δ) β × γ β × δ

                                                  Products distribute over sums as measurable spaces.

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

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

                                                    Equations
                                                    Instances For
                                                      def MeasurableEquiv.piCongrLeft {δ : Type u_4} {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (f : δ δ') :
                                                      ((b : δ) → π (f b)) ≃ᵐ ((a : δ') → π a)

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

                                                      Equations
                                                      Instances For
                                                        theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : δ δ') :
                                                        theorem MeasurableEquiv.piCongrLeft_apply_apply {ι : Type u_8} {ι' : Type u_9} (e : ι ι') {β : ι'Type u_10} [(i' : ι') → MeasurableSpace (β i')] (x : (i : ι) → β (e i)) (i : ι) :
                                                        (MeasurableEquiv.piCongrLeft (fun (i' : ι') => β i') e) x (e i) = x i
                                                        def MeasurableEquiv.arrowProdEquivProdArrow (α : Type u_8) (β : Type u_9) (γ : Type u_10) [MeasurableSpace α] [MeasurableSpace β] :
                                                        (γα × β) ≃ᵐ (γα) × (γβ)

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

                                                        Equations
                                                        Instances For
                                                          def MeasurableEquiv.arrowCongr' {α₁ : Type u_8} {β₁ : Type u_9} {α₂ : Type u_10} {β₂ : Type u_11} [MeasurableSpace β₁] [MeasurableSpace β₂] (hα : α₁ α₂) (hβ : β₁ ≃ᵐ β₂) :
                                                          (α₁β₁) ≃ᵐ (α₂β₂)

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

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

                                                            Pi-types are measurably equivalent to iterated products.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem MeasurableEquiv.piMeasurableEquivTProd_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), i l) :
                                                              @[simp]
                                                              theorem MeasurableEquiv.piMeasurableEquivTProd_symm_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), i l) :
                                                              def MeasurableEquiv.piUnique {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                              ((i : δ') → π i) ≃ᵐ π default

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

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                                (MeasurableEquiv.piUnique π).symm = uniqueElim
                                                                @[simp]
                                                                theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                                (MeasurableEquiv.piUnique π) = fun (f : (i : δ') → π i) => f default
                                                                def MeasurableEquiv.funUnique (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                                (αβ) ≃ᵐ β

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

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                                  (MeasurableEquiv.funUnique α β).symm = uniqueElim
                                                                  @[simp]
                                                                  theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                                  (MeasurableEquiv.funUnique α β) = fun (f : αβ) => f default
                                                                  def MeasurableEquiv.piFinTwo (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                  ((i : Fin 2) → α i) ≃ᵐ α 0 × α 1

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

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem MeasurableEquiv.piFinTwo_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                    (MeasurableEquiv.piFinTwo α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
                                                                    @[simp]
                                                                    theorem MeasurableEquiv.piFinTwo_symm_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                    (MeasurableEquiv.piFinTwo α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                                                                    def MeasurableEquiv.finTwoArrow {α : Type u_1} [MeasurableSpace α] :
                                                                    (Fin 2α) ≃ᵐ α × α

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

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem MeasurableEquiv.finTwoArrow_symm_apply {α : Type u_1} [MeasurableSpace α] :
                                                                      MeasurableEquiv.finTwoArrow.symm = fun (p : α × α) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                                                                      @[simp]
                                                                      theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [MeasurableSpace α] :
                                                                      MeasurableEquiv.finTwoArrow = fun (f : Fin 2α) => (f 0, f 1)
                                                                      def MeasurableEquiv.piFinSuccAbove {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
                                                                      ((j : Fin (n + 1)) → α j) ≃ᵐ α 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
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem MeasurableEquiv.piFinSuccAbove_symm_apply {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
                                                                        @[simp]
                                                                        theorem MeasurableEquiv.piFinSuccAbove_apply {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
                                                                        def MeasurableEquiv.piEquivPiSubtypeProd {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                        ((i : δ') → π i) ≃ᵐ ((i : Subtype p) → π i) × ((i : { i : δ' // ¬p i }) → π i)

                                                                        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
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem MeasurableEquiv.piEquivPiSubtypeProd_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                          (MeasurableEquiv.piEquivPiSubtypeProd π p) = fun (f : (i : δ') → π i) => (fun (x : { x : δ' // p x }) => f x, fun (x : { x : δ' // ¬p x }) => f x)
                                                                          @[simp]
                                                                          theorem MeasurableEquiv.piEquivPiSubtypeProd_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                          (MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun (f : ((i : { x : δ' // p x }) → π i) × ((i : { x : δ' // ¬p x }) → π i)) (x : δ') => if h : p x then f.1 x, h else f.2 x, h
                                                                          def MeasurableEquiv.sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
                                                                          ((i : δ δ') → α i) ≃ᵐ ((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
                                                                          Instances For
                                                                            theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
                                                                            theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
                                                                            def MeasurableEquiv.piOptionEquivProd {δ : Type u_8} (α : Option δType u_9) [(i : Option δ) → MeasurableSpace (α i)] :
                                                                            ((i : Option δ) → α i) ≃ᵐ ((i : δ) → α (some i)) × α 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.
                                                                            Instances For
                                                                              def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) :
                                                                              ((i : { x : δ' // x s }) → π i) × ((i : { x : δ' // x t }) → π i) ≃ᵐ ((i : { x : δ' // x s t }) → π i)

                                                                              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.
                                                                              Instances For
                                                                                def MeasurableEquiv.sumCompl {α : Type u_1} [MeasurableSpace α] {s : Set α} [DecidablePred fun (x : α) => x s] (hs : MeasurableSet s) :
                                                                                s s ≃ᵐ α

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

                                                                                Equations
                                                                                Instances For
                                                                                  def MeasurableEquiv.ofInvolutive {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) :
                                                                                  α ≃ᵐ α

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

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    @[simp]
                                                                                    theorem MeasurableEquiv.ofInvolutive_apply {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) (a : α) :
                                                                                    @[simp]
                                                                                    theorem MeasurableEquiv.ofInvolutive_symm {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) :
                                                                                    @[simp]
                                                                                    theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
                                                                                    MeasurableSpace.comap f inst✝ = inst✝¹
                                                                                    noncomputable def MeasurableEmbedding.equivImage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (s : Set α) (hf : MeasurableEmbedding f) :
                                                                                    s ≃ᵐ (f '' s)

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

                                                                                    Equations
                                                                                    Instances For
                                                                                      noncomputable def MeasurableEmbedding.equivRange {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
                                                                                      α ≃ᵐ (Set.range f)

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

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem MeasurableEmbedding.of_measurable_inverse_on_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : (Set.range f)α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g (Set.rangeFactorization 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) :
                                                                                        noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : βα} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) :
                                                                                        α ≃ᵐ β

                                                                                        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.
                                                                                        Instances For
                                                                                          theorem MeasurableSpace.comap_compl {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [BooleanAlgebra β] (h : Measurable compl) (f : αβ) :
                                                                                          MeasurableSpace.comap (fun (a : α) => (f a)) inferInstance = MeasurableSpace.comap f inferInstance
                                                                                          @[simp]
                                                                                          theorem MeasurableSpace.comap_not {α : Type u_1} (p : αProp) :
                                                                                          MeasurableSpace.comap (fun (a : α) => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance