Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.approxOn_range_nonneg

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] [inst_4 : Zero α] [inst_5 : Preorder α] {f : β → α},
  0 ≤ f →
    ∀ {hfm : Measurable f} [inst_6 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (n : ℕ),
      0 ≤ MeasureTheory.SimpleFunc.approxOn f hfm (Set.range f ∪ {0}) 0 ⋯ n

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDense

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpaceMeasurableSpaceZeroPreorderTopologicalSpace.SeparableSpace