Theorems · Theorem · measure theory
measurableSet_region_between_oc
∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)}The region between two measurable functions on a measurable set is measurable; a version for the region together with the graph of the upper function.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- Set.ofPredstatement · cited by 6,101
- MeasurableSetstatement and proof · cited by 3,075
- Measurablestatement and proof · cited by 1,499
- Set.Iocstatement · cited by 971
- Measurable.compproof · cited by 234
- MeasurableSet.interproof · cited by 167
- measurable_sndproof · cited by 94
- measurable_fstproof · cited by 79
- measurableSet_leproof · cited by 28
Cited by1
Results whose statement or proof uses this declaration.