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

• MeasureTheory.pack = if h : Countable A then MeasureTheory.embeddingReal A else ⇑(PolishSpace.measurableEquivOfNotCountable h ⋯)

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

• MeasureTheory.unpack = if h : Countable A then ⋯.invFun else ⇑(PolishSpace.measurableEquivOfNotCountable h ⋯).symm

@[simp]

theorem MeasureTheory.unpack_pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] (x : A) : unpack (pack x) = x

@[simp]

theorem MeasureTheory.pack_unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] (h : ¬Countable A) (x : ℝ) : pack (unpack x) = x

@[simp]

theorem MeasureTheory.measurable_pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] : Measurable pack

@[simp]

theorem MeasureTheory.measurable_unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] : Measurable unpack