Documentation Verification Report

OpenPos

📁 Source: Mathlib/MeasureTheory/Measure/OpenPos.lean

Statistics

Metric	Count
Definitions `IsOpenPosMeasure`	1
Theorems `ae_eq_iff_eq`, `isOpenPosMeasure_map`, `measure_ball_pos`, `measure_closedBall_pos`, `ae_eq_univ_iff_eq`, `measure_eq_one_iff_eq_univ`, `measure_eq_univ_iff_eq`, `of_isSigmaCompact_null`, `of_isClosed_null`, `ae_eq_empty_iff_eq`, `eq_empty_of_measure_zero`, `measure_eq_zero_iff`, `measure_ne_zero`, `measure_pos`, `measure_pos_iff`, `measure_zero_iff_eq_empty`, `isOpenPosMeasure`, `isOpenPosMeasure`, `comap`, `open_pos`, `dense_of_ae`, `eqOn_Icc_of_ae_eq`, `eqOn_Ico_of_ae_eq`, `eqOn_Ioc_of_ae_eq`, `eqOn_Ioo_of_ae_eq`, `eqOn_of_ae_eq`, `eqOn_open_of_ae_eq`, `eq_of_ae_eq`, `instNeZeroOfNonempty`, `interior_eq_empty_of_null`, `isOpenPosMeasure_smul`, `measure_Iio_pos`, `measure_Ioi_pos`, `measure_Ioo_eq_zero`, `measure_Ioo_pos`, `measure_pos_of_mem_nhds`, `measure_pos_of_nonempty_interior`, `measure_ball_pos`, `measure_closedBall_pos`, `measure_closedBall_pos_iff`, `measure_closedEBall_pos`, `measure_eball_pos`	42
Total	43

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_iff_eq` 📖	mathematical	`Continuous`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.eq_of_ae_eq` `Filter.EventuallyEq.rfl`
`isOpenPosMeasure_map` 📖	mathematical	`Continuous`	`MeasureTheory.Measure.IsOpenPosMeasure` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.map_apply` `measurable` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `IsOpen.measure_ne_zero` `IsOpen.preimage` `Function.Surjective.nonempty_preimage`

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_ball_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.eball`	—	`Metric.measure_eball_pos`
`measure_closedBall_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.closedEBall`	—	`Metric.measure_closedEBall_pos`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_univ_iff_eq` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set.univ`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.compl_empty_iff` `IsOpen.measure_eq_zero_iff` `isOpen_compl` `MeasureTheory.ae_eq_univ` `Filter.EventuallyEq.refl`
`measure_eq_one_iff_eq_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.univ`	—	`MeasureTheory.IsProbabilityMeasure.measure_univ` `measure_eq_univ_iff_eq` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure`
`measure_eq_univ_iff_eq` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.univ`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_eq_univ_iff_measure_eq` `MeasurableSet.nullMeasurableSet` `measurableSet` `ae_eq_univ_iff_eq`

IsMeagre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isSigmaCompact_null` 📖	mathematical	`IsSigmaCompact` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	`IsMeagre`	—	`MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_iUnion` `IsNowhereDense.of_isClosed_null` `IsCompact.isClosed` `isMeagre_iff_countable_union_isNowhereDense` `Set.countable_range` `instCountableNat` `Eq.subset` `Set.instReflSubset`

IsNowhereDense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isClosed_null` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	`IsNowhereDense`	—	`IsClosed.isNowhereDense_iff` `MeasureTheory.Measure.interior_eq_empty_of_null`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_empty_iff_eq` 📖	mathematical	`IsOpen`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set` `Set.instEmptyCollection`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_eq_empty` `measure_zero_iff_eq_empty`
`eq_empty_of_measure_zero` 📖	mathematical	`IsOpen` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	`Set.instEmptyCollection`	—	`measure_eq_zero_iff`
`measure_eq_zero_iff` 📖	mathematical	`IsOpen`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal` `Set.instEmptyCollection`	—	`ENNReal.instCanonicallyOrderedAdd` `measure_pos_iff`
`measure_ne_zero` 📖	—	`IsOpen` `Set.Nonempty`	—	—	`MeasureTheory.Measure.IsOpenPosMeasure.open_pos`
`measure_pos` 📖	mathematical	`IsOpen` `Set.Nonempty`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`Ne.bot_lt` `measure_ne_zero`
`measure_pos_iff` 📖	mathematical	`IsOpen`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.Nonempty`	—	`Set.nonempty_iff_ne_empty` `LT.lt.ne'` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `measure_pos`
`measure_zero_iff_eq_empty` 📖	mathematical	`IsOpen`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal` `Set.instEmptyCollection`	—	`measure_eq_zero_iff` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass`

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenPosMeasure` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.Measure.instPartialOrder`	`MeasureTheory.Measure.IsOpenPosMeasure`	—	`MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure` `absolutelyContinuous`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`IsOpenPosMeasure` 📖	CompData	18 math math: `IsOpenPosMeasure.neg`, `prod.instIsOpenPosMeasure`, `MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular`, `IsOpenPosMeasure.inv`, `MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_innerRegular`, `AbsolutelyContinuous.isOpenPosMeasure`, `Continuous.isOpenPosMeasure_map`, `LE.le.isOpenPosMeasure`, `MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular`, `IsHaarMeasure.toIsOpenPosMeasure`, `isOpenPosMeasure_smul`, `MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact`, `MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact`, `IsOpenPosMeasure.comap`, `toSphere.instIsOpenPosMeasure`, `MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular`, `IsAddHaarMeasure.toIsOpenPosMeasure`, `instIsOpenPosMeasureProdVolumeOfSFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_of_ae` 📖	mathematical	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`Dense` `setOf`	—	`instOuterMeasureClass` `dense_iff_closure_eq` `closure_eq_compl_interior_compl` `Set.compl_univ_iff` `interior_eq_empty_of_null`
`eqOn_Icc_of_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `restrict` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousOn`	`Set.EqOn`	—	`instOuterMeasureClass` `eqOn_of_ae_eq` `Eq.subset` `Set.instReflSubset` `closure_interior_Icc`
`eqOn_Ico_of_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `restrict` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousOn`	`Set.EqOn`	—	`instOuterMeasureClass` `eqOn_of_ae_eq` `Ico_subset_closure_interior`
`eqOn_Ioc_of_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `restrict` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousOn`	`Set.EqOn`	—	`instOuterMeasureClass` `eqOn_of_ae_eq` `Ioc_subset_closure_interior`
`eqOn_Ioo_of_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `restrict` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousOn`	`Set.EqOn`	—	`instOuterMeasureClass` `eqOn_of_ae_eq` `Ioo_subset_closure_interior` `OrderTopology.to_orderClosedTopology`
`eqOn_of_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `restrict` `ContinuousOn` `Set` `Set.instHasSubset` `closure` `interior`	`Set.EqOn`	—	`instOuterMeasureClass` `interior_subset` `Set.EqOn.of_subset_closure` `eqOn_open_of_ae_eq` `MeasureTheory.ae_restrict_of_ae_restrict_of_subset` `isOpen_interior` `ContinuousOn.mono`
`eqOn_open_of_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `restrict` `IsOpen` `ContinuousOn`	`Set.EqOn`	—	`instOuterMeasureClass` `MeasureTheory.ae_imp_of_ae_restrict` `isOpen_iff_mem_nhds` `Filter.inter_mem` `IsOpen.mem_nhds` `Filter.Tendsto.prodMk_nhds` `ContinuousOn.continuousAt` `IsClosed.isOpen_compl` `isClosed_diagonal` `Eq.le` `IsOpen.eq_empty_of_measure_zero`
`eq_of_ae_eq` 📖	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Continuous`	—	—	`instOuterMeasureClass` `eqOn_open_of_ae_eq` `MeasureTheory.ae_restrict_of_ae` `isOpen_univ` `Continuous.continuousOn`
`instNeZeroOfNonempty` 📖	mathematical	—	`MeasureTheory.Measure` `instZero`	—	`measure_univ_pos` `IsOpen.measure_pos` `isOpen_univ` `Set.univ_nonempty`
`interior_eq_empty_of_null` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `instZeroENNReal`	`interior` `Set.instEmptyCollection`	—	`IsOpen.eq_empty_of_measure_zero` `isOpen_interior` `MeasureTheory.measure_mono_null` `instOuterMeasureClass` `interior_subset`
`isOpenPosMeasure_smul` 📖	mathematical	—	`IsOpenPosMeasure` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `mul_ne_zero` `ENNReal.instNoZeroDivisors` `IsOpen.measure_ne_zero`
`measure_Iio_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Set.Iio` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measure_pos` `isOpen_Iio` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Set.nonempty_Iio`
`measure_Ioi_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Set.Ioi` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measure_pos` `isOpen_Ioi` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Set.nonempty_Ioi`
`measure_Ioo_eq_zero` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instZeroENNReal` `Preorder.toLE`	—	`IsOpen.measure_eq_zero_iff` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `Set.Ioo_eq_empty_iff` `not_lt`
`measure_Ioo_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Set.Ioo` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.measure_pos_iff` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `Set.nonempty_Ioo`
`measure_pos_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike`	—	`measure_pos_of_nonempty_interior` `mem_interior_iff_mem_nhds`
`measure_pos_of_nonempty_interior` 📖	mathematical	`Set.Nonempty` `interior`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike`	—	`LT.lt.trans_le` `IsOpen.measure_pos` `isOpen_interior` `MeasureTheory.measure_mono` `instOuterMeasureClass` `interior_subset`

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenPosMeasure` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.IsOpenPosMeasure`	—	`IsOpen.measure_ne_zero`

MeasureTheory.Measure.IsOpenPosMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	`Topology.IsOpenEmbedding`	`MeasureTheory.Measure.IsOpenPosMeasure` `MeasureTheory.Measure.comap`	—	`MeasurableEmbedding.comap_apply` `Topology.IsOpenEmbedding.measurableEmbedding` `open_pos` `Topology.IsOpenEmbedding.isOpen_iff_image_isOpen` `Set.Nonempty.image`
`open_pos` 📖	—	`IsOpen` `Set.Nonempty`	—	—	—

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_ball_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ball`	—	`IsOpen.measure_pos` `isOpen_ball` `nonempty_ball`
`measure_closedBall_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `closedBall`	—	`LT.lt.trans_le` `measure_ball_pos` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `ball_subset_closedBall`
`measure_closedBall_pos_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `closedBall` `MetricSpace.toPseudoMetricSpace` `Real` `Real.instLT` `Real.instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Set.Subsingleton.measure_zero` `subsingleton_closedBall` `le_refl` `measure_closedBall_pos`
`measure_closedEBall_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `closedEBall`	—	`LT.lt.trans_le` `measure_eball_pos` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `eball_subset_closedEBall`
`measure_eball_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `eball`	—	`IsOpen.measure_pos` `isOpen_eball` `mem_eball_self` `Ne.bot_lt`

---

← Back to Index