structure FlatReal : Type

Reals with the Lebesgue measure and a discrete ωCPO structure.

• val : ℝ

  The underlying real number.

instance FlatReal.instInhabited : Inhabited FlatReal

Equations

• FlatReal.instInhabited = { default := { val := 0 } }

instance FlatReal.instMeasurableSpace : MeasurableSpace FlatReal

Equations

• FlatReal.instMeasurableSpace = MeasurableSpace.comap FlatReal.val inferInstance

noncomputable instance FlatReal.instMeasureSpace : MeasureTheory.MeasureSpace FlatReal

Equations

• FlatReal.instMeasureSpace = { toMeasurableSpace := FlatReal.instMeasurableSpace, volume := MeasureTheory.Measure.map FlatReal.mk MeasureTheory.volume }

@[simp]

theorem FlatReal.R.measurable_mk : Measurable mk

@[simp]

theorem FlatReal.R.measurable_val : Measurable val

instance FlatReal.instSigmaFiniteVolume : MeasureTheory.SigmaFinite MeasureTheory.volume

instance FlatReal.instQuasiBorelSpace : QuasiBorelSpace FlatReal

Equations

• FlatReal.instQuasiBorelSpace = QuasiBorelSpace.ofMeasurableSpace

instance FlatReal.instPartialOrder : PartialOrder FlatReal

Equations

• FlatReal.instPartialOrder = { le := fun (x y : FlatReal) => x = y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := FlatReal.instPartialOrder._proof_1, le_antisymm := ⋯ }

instance FlatReal.instOmegaCompletePartialOrder : OmegaCompletePartialOrder FlatReal

FlatReal is trivially an ωCPO: chains are constant by discreteness.

Equations

• One or more equations did not get rendered due to their size.

instance FlatReal.instOmegaQuasiBorelSpace : OmegaQuasiBorelSpace FlatReal

FlatReal is trivially an ωQBS.

Equations

• One or more equations did not get rendered due to their size.

instance FlatReal.instTopologicalSpace : TopologicalSpace FlatReal

Equations

• FlatReal.instTopologicalSpace = TopologicalSpace.induced FlatReal.val inferInstance

instance FlatReal.instBorelSpace : BorelSpace FlatReal

instance FlatReal.instPolishSpace : PolishSpace FlatReal

instance FlatReal.instStandardBorelSpace : StandardBorelSpace FlatReal

@[simp]

theorem FlatReal.le_iff_eq {x y : FlatReal} : x ≤ y ↔ x = y

@[simp]

theorem FlatReal.ωScottContinuous_of {A : Type u_1} [OmegaCompletePartialOrder A] (f : FlatReal → A) : OmegaCompletePartialOrder.ωScottContinuous f