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.injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (self : MeasurableEmbedding f) :

    A measurable embedding is injective.

    theorem MeasurableEmbedding.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (self : MeasurableEmbedding f) :

    A measurable embedding is a measurable function.

    theorem MeasurableEmbedding.measurableSet_image' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (self : MeasurableEmbedding f) ⦃s : Set α :

    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) :
    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.exists_measurable_proj {α : Type u_1} {s : Set α} :
    ∀ {x : MeasurableSpace α}, MeasurableSet ss.Nonempty∃ (f : αs), Measurable f ∀ (x : s), f x = 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 self.toEquiv

      The forward function of a measurable equivalence is measurable.

    • measurable_invFun : Measurable self.symm

      The inverse function of a measurable equivalence is measurable.

    Instances For
      theorem MeasurableEquiv.measurable_toFun {α : Type u_6} {β : Type u_7} [MeasurableSpace α] [MeasurableSpace β] (self : α ≃ᵐ β) :
      Measurable self.toEquiv

      The forward function of a measurable equivalence is measurable.

      theorem MeasurableEquiv.measurable_invFun {α : Type u_6} {β : Type u_7} [MeasurableSpace α] [MeasurableSpace β] (self : α ≃ᵐ β) :
      Measurable self.symm

      The inverse function of a measurable equivalence is measurable.

      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_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ : α ≃ᵐ β} {e₂ : α ≃ᵐ β} :
                  e₁ = e₂ e₁ = e₂
                  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} {β : 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
                                                        @[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.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.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.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.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                            (MeasurableEquiv.funUnique α β) = fun (f : αβ) => f default
                                                            @[simp]
                                                            theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                            (MeasurableEquiv.funUnique α β).symm = uniqueElim
                                                            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.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.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.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.finTwoArrow {α : Type u_1} [MeasurableSpace α] :
                                                                (Fin 2α) ≃ᵐ α × α

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

                                                                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.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.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
                                                                    @[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)
                                                                    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
                                                                      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 : Finset δ'} {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
                                                                              @[simp]
                                                                              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]
                                                                                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