Theorems · Theorem · measure theory
integrableOn_Ici_iff_integrableOn_Ioi
∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
[inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
{f : α → ε'} {μ : MeasureTheory.Measure α} {b : α} [MeasureTheory.NullSingletonClass μ],
autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Ici_iff_integrableOn_Ioi._auto_1 →
(MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- PartialOrderstatement and proof · cited by 6,410
- Set.Ioistatement · cited by 1,463
- Set.Icistatement · cited by 1,070
- ENorm.enormstatement and proof · cited by 715
- MeasureTheory.IntegrableOnstatement · cited by 548
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- MeasurableSingletonClassstatement and proof · cited by 230
Cited by7
Results whose statement or proof uses this declaration.
- integrable_rpow_mul_exp_neg_mul_sqproof · cited by 2
- MeasureTheory.integral_deriv_smul_comp_Ioiproof · cited by 2
- integral_comp_absproof · cited by 2
- integrableOn_exp_neg_Ioiproof · cited by 1
- integrable_of_isBigO_exp_negproof · cited by 1
- tendsto_sum_mul_atTop_nhds_one_sub_integralproof · cited by 0
- tendsto_sum_mul_atTop_nhds_one_sub_integral₀proof · cited by 0