Theorems · Inductive type · measure theory
MeasureTheory.Measure.IsOpenPosMeasure
{X : Type u_1} → [TopologicalSpace X] → {m : MeasurableSpace X} → MeasureTheory.Measure X → PropA measure is said to be IsOpenPosMeasure if it is positive on nonempty open sets.
- Defined in
- Mathlib.MeasureTheory.Measure.OpenPos
- Cited by
- 80 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by86
Results whose statement or proof uses this declaration.
- IsOpen.measure_posstatement and proof · cited by 18
- Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzerostatement and proof · cited by 11
- Metric.measure_closedBall_posstatement and proof · cited by 8
- IsOpen.measure_eq_zero_iffstatement and proof · cited by 6
- IsOpen.measure_ne_zerostatement and proof · cited by 6
- MeasureTheory.Measure.IsOpenPosMeasure.open_posstatement and proof · cited by 6
- Metric.measure_ball_posstatement and proof · cited by 5
- ContDiffBump.support_normed_eqstatement and proof · cited by 5
- MeasureTheory.Measure.eqOn_of_ae_eqstatement and proof · cited by 4
- Continuous.isOpenPosMeasure_mapstatement and proof · cited by 4
- ContDiffBump.integral_normedstatement and proof · cited by 4
- Continuous.ae_eq_iff_eqstatement and proof · cited by 4