Theorems · Theorem · measure theory
measurableSet_Ioo
∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
{a b : α} [OrderClosedTopology α], MeasurableSet (Set.Ioo a b)- Cited by
- 42 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- LinearOrderstatement and proof · cited by 8,572
- MeasurableSetstatement · cited by 3,075
- Set.Ioostatement · cited by 1,214
- OpensMeasurableSpacestatement and proof · cited by 636
- OrderClosedTopologystatement and proof · cited by 445
- IsOpen.measurableSetproof · cited by 82
- isOpen_Iooproof · cited by 54
Cited by42
Results whose statement or proof uses this declaration.
- Manifold.pathELength_eq_lintegral_mfderivWithin_Iccproof · cited by 5
- intervalIntegral.integral_deriv_of_contDiffOn_Iccproof · cited by 4
- intervalIntegral.integral_mono_on_of_le_Iooproof · cited by 4
- intervalIntegral.integrableOn_Ioo_rpow_iffproof · cited by 3
- intervalIntegral.intervalIntegrable_cpowproof · cited by 2
- MeasureTheory.posConvolution_eq_convolution_indicatorproof · cited by 2
- StieltjesFunction.measure_Icoproof · cited by 2
- MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_leproof · cited by 2
- measure_eq_measure_preimage_add_measure_tsum_Ico_zpowproof · cited by 2
- Real.smul_map_volume_mul_leftproof · cited by 2
- Manifold.pathELength_congr_Iooproof · cited by 2
- curveIntegralFun_trans_aeeq_leftproof · cited by 2