Borel measurable space on WithTop

For ι a linear order with the order topology, we define the Borel measurable space on WithTop ι. We then prove that the natural inclusion ι → WithTop ι is measurable, and that the function WithTop.untopA : WithTop ι → ι (which sends ⊤ to an arbitrary element of ι) is measurable.

Main statements

• measurable_of_measurable_comp_coe: if f : WithTop ι → α is such that f ∘ coe is measurable, then f is measurable.
• Measurable.withTop_coe: the function fun x : ι ↦ (x : WithTop ι) is measurable.
• Measurable.untopD: for d : ι, the function WithTop.untopD d : WithTop ι → ι is measurable.
• Measurable.untopA: the function WithTop.untopA : WithTop ι → ι is measurable.

instance WithTop.instMeasurableSpace {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : MeasurableSpace (WithTop ι)

Equations

• WithTop.instMeasurableSpace = borel (WithTop ι)

instance WithTop.instBorelSpace {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : BorelSpace (WithTop ι)

noncomputable def WithTop.MeasurableEquiv.neTopEquiv {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] : ↑{r : WithTop ι | r ≠ ⊤} ≃ᵐ ι

Measurable equivalence between the non-top elements of WithTop ι and ι.

Equations

• WithTop.MeasurableEquiv.neTopEquiv = (WithTop.neTopHomeomorph ι).toMeasurableEquiv

theorem WithTop.measurable_of_measurable_comp_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} {f : WithTop ι → α} (h : Measurable fun (p : ι) => f ↑p) : Measurable f

theorem WithTop.measurable_untopD {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] (d : ι) : Measurable (untopD d)

theorem WithTop.measurable_untopA {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] [Nonempty ι] : Measurable untopA

theorem WithTop.measurable_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] : Measurable fun (x : ι) => ↑x

theorem Measurable.withTop_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} {f : α → ι} (hf : Measurable f) : Measurable fun (x : α) => ↑(f x)

theorem Measurable.untopD {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} (d : ι) {f : α → WithTop ι} (hf : Measurable f) : Measurable fun (x : α) => WithTop.untopD d (f x)

theorem Measurable.untopA {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} [Nonempty ι] {f : α → WithTop ι} (hf : Measurable f) : Measurable fun (x : α) => (f x).untopA

def WithTop.measurableEquivSum {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] : WithTop ι ≃ᵐ ι ⊕ Unit

Measurable equivalence between WithTop ι and ι ⊕ Unit.

Equations

• WithTop.measurableEquivSum = { toEquiv := Equiv.optionEquivSumPUnit ι, measurable_toFun := ⋯, measurable_invFun := ⋯ }