Theorems · Theorem · measure theory
measurableSet_Ioc
∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
{a b : α} [ClosedIicTopology α], MeasurableSet (Set.Ioc a b)- Cited by
- 65 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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.Iocstatement · cited by 971
- OpensMeasurableSpacestatement and proof · cited by 636
- MeasurableSet.interproof · cited by 167
- ClosedIicTopologystatement and proof · cited by 115
- measurableSet_Ioiproof · cited by 83
- measurableSet_Iicproof · cited by 23
Cited by65
Results whose statement or proof uses this declaration.
- measurableSet_uIocproof · cited by 20
- intervalIntegral.integral_congrproof · cited by 18
- IntervalIntegrable.continuousOn_mulproof · cited by 8
- StieltjesFunction.measure_Iccproof · cited by 8
- IntervalIntegrable.mul_continuousOnproof · cited by 7
- intervalIntegral.intervalIntegrable_cpow'proof · cited by 7
- BoundedVariationOn.vectorMeasure_Iccproof · cited by 6
- IntervalIntegrable.continuousOn_smulproof · cited by 6
- intervalIntegral.intervalIntegrable_rpow'proof · cited by 6
- BoxIntegral.Box.measurableSet_coeproof · cited by 5
- intervalIntegral.integral_mono_onproof · cited by 5
- fourierCoeffOn_eq_integralproof · cited by 5