Structures · Analysis
MeasureTheory.Measure.IsOpenPosMeasure
A measure is said to be IsOpenPosMeasure if it is positive on nonempty open sets.
- Defined in
- Mathlib.MeasureTheory.Measure.OpenPos
- Shape
- One type argument · adds open_pos
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances2
- Prod
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by76
- IsOpen.measure_pos
- Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
- Metric.measure_closedBall_pos
- MeasureTheory.Measure.IsOpenPosMeasure.open_pos
- IsOpen.measure_ne_zero
- IsOpen.measure_eq_zero_iff
- Metric.measure_ball_pos
- ContDiffBump.support_normed_eq
- Continuous.ae_eq_iff_eq
- Continuous.isOpenPosMeasure_map
- ContDiffBump.integral_normed
- MeasureTheory.Measure.eqOn_of_ae_eq
- MeasureTheory.Measure.measure_pos_of_nonempty_interior
- ContDiffBump.integral_pos
- MeasureTheory.Measure.measure_pos_of_mem_nhds
- IsOpen.eq_empty_of_measure_zero
- MeasureTheory.measure_univ_of_isAddLeftInvariant
- Metric.measure_eball_pos
- ContinuousMap.hasSum_of_hasSum_Lp
- MeasureTheory.Measure.interior_eq_empty_of_null
- ContinuousMap.toLp_injective
- IsOpen.isEverywherePos
- IsClosed.measure_eq_univ_iff_eq
- IsOpen.measure_pos_iff
- MeasureTheory.Measure.isOpenPosMeasure_smul
- MeasureTheory.Measure.eqOn_open_of_ae_eq
- MeasureTheory.measure_univ_of_isMulLeftInvariant
- DenseRange.zsmul_of_ergodic_add_left
- DenseRange.zpow_of_ergodic_mul_left
- MeasureTheory.Measure.measure_Ioo_pos
- MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo
- tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn
- IsClosed.ae_eq_univ_iff_eq
- Metric.measure_closedEBall_pos
- ContDiffBump.tendsto_support_normed_smallSets
- BoundedContinuousFunction.toLp_inj
- MeasureTheory.Measure.dense_of_ae
- MeasureTheory.integral_pos_of_integrable_nonneg_nonzero
- MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure
- MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo
- tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
- IsNowhereDense.of_isClosed_null
- ContDiffBump.hasCompactSupport_normed
- IsOpen.measure_zero_iff_eq_empty
- ContDiffBump.tsupport_normed_eq
- BoundedContinuousFunction.toLp_injective
- MeasureTheory.Measure.eqOn_Icc_of_ae_eq
- ContDiffBump.integral_normed_smul
- MeasureTheory.Measure.eq_of_ae_eq
- MeasureTheory.Measure.instNeZeroOfNonempty
Ancestors0
No ancestors.