Theorems · Theorem · measure theory
measurableSet_Ioi
∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
{a : α} [ClosedIicTopology α], MeasurableSet (Set.Ioi a)- Cited by
- 83 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.Ioistatement · cited by 1,463
- OpensMeasurableSpacestatement and proof · cited by 636
- ClosedIicTopologystatement and proof · cited by 115
- IsOpen.measurableSetproof · cited by 82
- isOpen_Ioiproof · cited by 43
Cited by83
Results whose statement or proof uses this declaration.
- measurableSet_Iocproof · cited by 65
- Real.Gamma_pos_of_posproof · cited by 17
- IsStrongFEPair.Λ_eqproof · cited by 6
- Real.Gamma_one_half_eqproof · cited by 6
- MeasureTheory.integral_comp_mul_left_Ioiproof · cited by 5
- MeasureTheory.integrableOn_Ioi_comp_mul_left_iffproof · cited by 5
- MeasureTheory.aecover_Ioiproof · cited by 5
- integral_rpow_mul_exp_neg_rpowproof · cited by 4
- MeasureTheory.integral_of_hasDerivAt_of_tendstoproof · cited by 4
- AntitoneOn.sum_Ico_le_integralproof · cited by 3
- intervalIntegral.integral_interval_add_Ioiproof · cited by 3
- Complex.GammaIntegral_convergentproof · cited by 3