theorem SimpleApproximation.eapprox_uniform_on_bounded_strict {X : Type u_1} [MeasurableSpace X] {f : X → ENNReal} (hf : Measurable f) (c : NNReal) (ε : ENNReal) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (x : X), f x ≤ ↑c → f x - (MeasureTheory.SimpleFunc.eapprox f n) x < ε

Strict uniform approximation by the canonical simple-function approximants SimpleFunc.eapprox: for any ε > 0 there exists an index N such that for all n ≥ N, the approximation error f x − eapprox f n x is strictly less than ε uniformly over the bounded sublevel set {x | f x ≤ c}.