Lemmas about the unit interval

theorem doubleton_eq (s : Set ↑{0, 1}) : s = ∅ ∨ s = {⟨0, doubleton_eq._proof_1⟩} ∨ s = {⟨1, doubleton_eq._proof_2⟩} ∨ s = {⟨0, doubleton_eq._proof_1⟩, ⟨1, doubleton_eq._proof_2⟩}

theorem doubleton_univ : {⟨0, doubleton_eq._proof_1⟩, ⟨1, doubleton_eq._proof_2⟩} = Set.univ

theorem doubleton_union_univ : {⟨0, doubleton_eq._proof_1⟩} ∪ {⟨1, doubleton_eq._proof_2⟩} = Set.univ

theorem measure_doubleton_eq_add (μ : MeasureTheory.Measure ↑{0, 1}) : μ = μ {⟨0, doubleton_eq._proof_1⟩} • MeasureTheory.Measure.dirac ⟨0, doubleton_eq._proof_1⟩ + μ {⟨1, doubleton_eq._proof_2⟩} • MeasureTheory.Measure.dirac ⟨1, doubleton_eq._proof_2⟩

theorem doubleton_lintegral {μ : MeasureTheory.Measure ↑{0, 1}} {f : ↑{0, 1} → ENNReal} : ∫⁻ (x : ↑{0, 1}), f x ∂μ = μ {⟨0, doubleton_eq._proof_1⟩} * f ⟨0, doubleton_eq._proof_1⟩ + μ {⟨1, doubleton_eq._proof_2⟩} * f ⟨1, doubleton_eq._proof_2⟩

theorem unitInterval.zero_one_mem {x : ↑{0, 1}} : ↑x ∈ unitInterval

def unitInterval.doubleton (x : ↑{0, 1}) : { x : ℝ // x ∈ unitInterval }

Define the embedding from the doubleton set {0, 1} into the unit interval I

Equations

• unitInterval.doubleton x = ⟨↑x, ⋯⟩

theorem unitInterval.doubleton_emb : MeasurableEmbedding doubleton

theorem unitInterval.measurable_doubleton : Measurable doubleton