Theorems · Theorem · measure theory

measurable_liftCover

∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι]
  (t : ι → Set α),
  (∀ (i : ι), MeasurableSet (t i)) →
    ∀ (f : (i : ι) → ↑(t i) → β),
      (∀ (i : ι), Measurable (f i)) →
        ∀ (hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
          (htU : ⋃ i, t i = Set.univ), Measurable (Set.liftCover t f hf htU)

Let t i be a countable covering of α by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.liftCover t f _ _, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Countable