Theorems · Theorem · measure theory
measurableSet_Iio
∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
{a : α} [ClosedIciTopology α], MeasurableSet (Set.Iio a)- Cited by
- 12 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, 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.Iiostatement · cited by 1,166
- OpensMeasurableSpacestatement and proof · cited by 636
- ClosedIciTopologystatement and proof · cited by 156
- IsOpen.measurableSetproof · cited by 82
- isOpen_Iioproof · cited by 38
Cited by12
Results whose statement or proof uses this declaration.
- measurableSet_Icoproof · cited by 17
- ProbabilityTheory.lintegral_gammaPDF_eq_oneproof · cited by 2
- MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEqproof · cited by 1
- ProbabilityTheory.lintegral_paretoPDF_of_leproof · cited by 1
- MeasureTheory.aecover_Iio_of_Icoproof · cited by 1
- MeasureTheory.IntegrableOn.continuousWithinAt_Iic_primitive_Iioproof · cited by 1
- BoundedVariationOn.vectorMeasure_Iioproof · cited by 1
- ProbabilityTheory.lintegral_betaPDFproof · cited by 1
- MeasureTheory.Measure.volumeIoiPow_apply_Iioproof · cited by 1
- ProbabilityTheory.lintegral_gammaPDF_of_nonposproof · cited by 1
- nullMeasurableSet_Iioproof · cited by 0
- BoundedVariationOn.vectorMeasure_univproof · cited by 0