Documentation

QuasiBorelSpaces.MeasureTheory.Pack

source
noncomputable def MeasureTheory.pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] :
A → ℝ

Packs a natural number and a real number into a single real number.

Equations
Instances For
    source
    noncomputable def MeasureTheory.unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] :
    ℝ → A

    Unpacks a natural number and a real number from a single real number.

    Equations
    Instances For
      source
      @[simp]
      theorem MeasureTheory.unpack_pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] (x : A) :
      unpack (pack x) = x
      source
      @[simp]
      theorem MeasureTheory.measurable_pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] :
      Measurable pack
      source
      @[simp]
      theorem MeasureTheory.measurable_unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] :
      Measurable unpack