Theorems · Theorem · measure theory

RealRMK.range_cut_partition

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X]
  (f : CompactlySupportedContinuousMap X ℝ) (a : ℝ) {ε : ℝ},
  0 < ε →
    ∀ (N : ℕ),
      Set.range ⇑f ⊆ Set.Ioo a (a + ↑N * ε) →
        ∃ E,
          tsupport ⇑f = ⋃ j, E j ∧
            Set.univ.PairwiseDisjoint E ∧
              (∀ (n : Fin N), ∀ x ∈ E n, a + ε * ↑↑n < f x ∧ f x ≤ a + ε * (↑↑n + 1)) ∧
                ∀ (n : Fin N), MeasurableSet (E n)

Given f : C_c(X, ℝ) such that range f ⊆ [a, b] we obtain a partition of the support of f determined by partitioning [a, b] into N pieces.

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpace