Documentation Verification Report

EverywherePos

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

Statistics

Metric	Count
Definitions `IsEverywherePos`, `everywherePosSubset`	2
Theorems `everywherePosSubset`, `everywherePosSubset`, `isEverywherePos`, `everywherePosSubset`, `IsGdelta_of_isAddLeftInvariant`, `IsGdelta_of_isMulLeftInvariant`, `of_forall_exists_nhds_eq`, `smul_measure`, `smul_measure_nnreal`, `everywherePosSubset_ae_eq`, `everywherePosSubset_ae_eq_of_measure_ne_top`, `everywherePosSubset_subset`, `exists_isOpen_everywherePosSubset_eq_diff`, `innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup`, `innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group`, `isEverywherePos_everywherePosSubset`, `isEverywherePos_everywherePosSubset_of_measure_ne_top`, `isEverywherePos_iff_of_forall_exists_nhds_eq`, `measure_eq_zero_of_subset_diff_everywherePosSubset`	19
Total	21

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`everywherePosSubset` 📖	mathematical	—	`IsClosed` `MeasureTheory.Measure.everywherePosSubset`	—	`MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff` `sdiff`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`everywherePosSubset` 📖	mathematical	`IsCompact`	`MeasureTheory.Measure.everywherePosSubset`	—	`MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff` `diff`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEverywherePos` 📖	mathematical	`IsOpen`	`MeasureTheory.Measure.IsEverywherePos`	—	`mem_nhdsWithin` `lt_of_lt_of_le` `measure_pos` `inter` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`everywherePosSubset` 📖	mathematical	`MeasurableSet`	`MeasureTheory.Measure.everywherePosSubset`	—	`MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff` `diff` `IsOpen.measurableSet`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`IsEverywherePos` 📖	MathDef	4 math math: `isEverywherePos_everywherePosSubset_of_measure_ne_top`, `isEverywherePos_iff_of_forall_exists_nhds_eq`, `isEverywherePos_everywherePosSubset`, `IsOpen.isEverywherePos`
`everywherePosSubset` 📖	CompOp	9 math math: `MeasurableSet.everywherePosSubset`, `isEverywherePos_everywherePosSubset_of_measure_ne_top`, `everywherePosSubset_ae_eq`, `IsClosed.everywherePosSubset`, `isEverywherePos_everywherePosSubset`, `everywherePosSubset_ae_eq_of_measure_ne_top`, `IsCompact.everywherePosSubset`, `everywherePosSubset_subset`, `exists_isOpen_everywherePosSubset_eq_diff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`everywherePosSubset_ae_eq` 📖	mathematical	`MeasurableSet`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `everywherePosSubset`	—	`instOuterMeasureClass` `Set.diff_eq_empty` `everywherePosSubset_subset` `MeasureTheory.measure_empty` `MeasurableSet.measure_eq_iSup_isCompact` `MeasurableSet.diff` `MeasurableSet.everywherePosSubset` `measure_eq_zero_of_subset_diff_everywherePosSubset`
`everywherePosSubset_ae_eq_of_measure_ne_top` 📖	mathematical	`MeasurableSet`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `everywherePosSubset`	—	`LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.diff_subset` `Ne.lt_top` `Set.diff_eq_empty` `everywherePosSubset_subset` `MeasureTheory.measure_empty` `MeasurableSet.measure_eq_iSup_isCompact_of_ne_top` `MeasurableSet.diff` `MeasurableSet.everywherePosSubset` `measure_eq_zero_of_subset_diff_everywherePosSubset`
`everywherePosSubset_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `everywherePosSubset`	—	—
`exists_isOpen_everywherePosSubset_eq_diff` 📖	mathematical	—	`IsOpen` `everywherePosSubset` `Set` `Set.instSDiff`	—	`isOpen_iff_mem_nhds` `mem_nhdsWithin_iff_exists_mem_nhds_inter` `mem_nhds_iff` `inter_mem_nhdsWithin` `IsOpen.mem_nhds` `MeasureTheory.measure_mono_null` `instOuterMeasureClass` `Set.inter_comm` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_inter_left` `Filter.mem_of_superset` `Set.ext` `ENNReal.instCanonicallyOrderedAdd`
`innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup` 📖	mathematical	—	`InnerRegularWRT` `Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero` `Set` `Set.preimage` `Set.instSingletonSet` `Real.instOne` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `Top.top` `instTopENNReal`	—	`InnerRegularWRT.trans` `IsCompact.everywherePosSubset` `IsClosed.everywherePosSubset` `everywherePosSubset_subset` `isEverywherePos_everywherePosSubset_of_measure_ne_top` `BorelSpace.opensMeasurable` `IsClosed.measurableSet` `LT.lt.ne` `IsCompact.measure_lt_top` `IsEverywherePos.IsGdelta_of_isAddLeftInvariant` `exists_continuous_one_zero_of_isCompact_of_isGδ` `IsTopologicalAddGroup.regularSpace` `isClosed_empty` `Set.disjoint_empty` `MeasureTheory.measure_congr` `instOuterMeasureClass` `everywherePosSubset_ae_eq_of_measure_ne_top` `MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup`
`innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group` 📖	mathematical	—	`InnerRegularWRT` `Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero` `Set` `Set.preimage` `Set.instSingletonSet` `Real.instOne` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `Top.top` `instTopENNReal`	—	`InnerRegularWRT.trans` `IsCompact.everywherePosSubset` `IsClosed.everywherePosSubset` `everywherePosSubset_subset` `isEverywherePos_everywherePosSubset_of_measure_ne_top` `BorelSpace.opensMeasurable` `IsClosed.measurableSet` `LT.lt.ne` `IsCompact.measure_lt_top` `IsEverywherePos.IsGdelta_of_isMulLeftInvariant` `exists_continuous_one_zero_of_isCompact_of_isGδ` `IsTopologicalGroup.regularSpace` `isClosed_empty` `Set.disjoint_empty` `MeasureTheory.measure_congr` `instOuterMeasureClass` `everywherePosSubset_ae_eq_of_measure_ne_top` `MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group`
`isEverywherePos_everywherePosSubset` 📖	mathematical	`MeasurableSet`	`IsEverywherePos` `everywherePosSubset`	—	`mem_nhdsWithin_iff_exists_mem_nhds_inter` `Set.inter_comm` `inter_mem_nhdsWithin` `instOuterMeasureClass` `MeasureTheory.ae_eq_set_inter` `MeasureTheory.ae_eq_refl` `everywherePosSubset_ae_eq` `LT.lt.trans_le` `Filter.EventuallyEq.measure_eq` `MeasureTheory.measure_mono`
`isEverywherePos_everywherePosSubset_of_measure_ne_top` 📖	mathematical	`MeasurableSet`	`IsEverywherePos` `everywherePosSubset`	—	`mem_nhdsWithin_iff_exists_mem_nhds_inter` `Set.inter_comm` `inter_mem_nhdsWithin` `instOuterMeasureClass` `MeasureTheory.ae_eq_set_inter` `MeasureTheory.ae_eq_refl` `everywherePosSubset_ae_eq_of_measure_ne_top` `LT.lt.trans_le` `Filter.EventuallyEq.measure_eq` `MeasureTheory.measure_mono`
`isEverywherePos_iff_of_forall_exists_nhds_eq` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `instFunLike`	`IsEverywherePos`	—	`IsEverywherePos.of_forall_exists_nhds_eq`
`measure_eq_zero_of_subset_diff_everywherePosSubset` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `Set.instSDiff` `everywherePosSubset`	`DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `instFunLike` `instZeroENNReal`	—	`IsCompact.induction_on` `MeasureTheory.measure_empty` `instOuterMeasureClass` `MeasureTheory.measure_mono_null` `MeasureTheory.measure_union_null` `ENNReal.instCanonicallyOrderedAdd` `nhdsWithin_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset`

MeasureTheory.Measure.IsEverywherePos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsGdelta_of_isAddLeftInvariant` 📖	mathematical	`MeasureTheory.Measure.IsEverywherePos` `IsCompact`	`IsGδ`	—	`exists_seq_strictAnti_tendsto'` `ENNReal.instOrderTopology` `ENNReal.instDenselyOrdered` `TopologicalSpace.SecondCountableTopology.to_firstCountableTopology` `ENNReal.instSecondCountableTopology` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.one` `exists_open_nhds_zero_add_subset` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt` `LT.lt.ne'` `IsCompact.exists_mapClusterPt` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.le_principal_iff` `Filter.mem_map` `Filter.mem_atTop_sets` `Set.mem_preimage` `le_of_lt` `IsOpen.mem_nhds` `IsOpen.add_right` `VAddCommClass.continuousConstVAdd` `AddSemigroup.opposite_vaddCommClass` `Set.add_singleton` `Set.image_add_right` `add_neg_cancel` `Filter.Frequently.exists` `Filter.Frequently.and_eventually` `MapClusterPt.frequently` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Set.iInter₂_subset` `Finset.mem_range` `add_neg_cancel_right` `neg_one_zsmul` `add_assoc` `Mathlib.Tactic.Group.zsmul_trick_zero'` `neg_add_cancel` `zero_zsmul` `add_zero` `le_antisymm` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Filter.Eventually.of_forall` `bot_le` `MeasureTheory.measure_vadd` `MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure` `Set.vadd_set_sdiff` `vadd_vadd` `one_add_zsmul` `neg_zsmul` `one_zsmul` `zero_vadd` `inter_mem_nhdsWithin` `isOpen_compl_iff` `IsClosed.vadd` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `Set.mem_compl_iff` `Mathlib.Tactic.Contrapose.contrapose₄` `Set.mem_vadd_set_iff_neg_vadd_mem` `neg_add_rev` `neg_neg` `neg_add_cancel_right` `lt_irrefl` `LE.le.trans_lt` `Eq.le` `Set.mem_iInter` `Set.Subset.antisymm` `Set.subset_iInter_iff` `Set.subset_add_right` `Set.iInter_congr_Prop` `IsGδ.iInter_of_isOpen` `instCountableNat` `isOpen_biInter_finset`
`IsGdelta_of_isMulLeftInvariant` 📖	mathematical	`MeasureTheory.Measure.IsEverywherePos` `IsCompact`	`IsGδ`	—	`exists_seq_strictAnti_tendsto'` `ENNReal.instOrderTopology` `ENNReal.instDenselyOrdered` `TopologicalSpace.SecondCountableTopology.to_firstCountableTopology` `ENNReal.instSecondCountableTopology` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.one` `exists_open_nhds_one_mul_subset` `IsTopologicalGroup.toContinuousMul` `MeasureTheory.eventually_nhds_one_measure_smul_diff_lt` `LT.lt.ne'` `IsCompact.exists_mapClusterPt` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `le_of_lt` `IsOpen.mem_nhds` `IsOpen.mul_right` `SMulCommClass.continuousConstSMul` `Semigroup.opposite_smulCommClass` `Set.mul_singleton` `Set.image_mul_right` `mul_inv_cancel` `Filter.Frequently.exists` `Filter.Frequently.and_eventually` `MapClusterPt.frequently` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Set.iInter₂_subset` `mul_inv_cancel_right` `Mathlib.Tactic.Group.zpow_trick_one'` `neg_add_cancel` `zpow_zero` `mul_one` `le_antisymm` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Filter.Eventually.of_forall` `bot_le` `MeasureTheory.measure_smul` `MeasureTheory.Measure.IsMulLeftInvariant.smulInvariantMeasure` `Set.smul_set_sdiff` `smul_smul` `add_neg_cancel` `zpow_neg` `zpow_one` `one_smul` `inter_mem_nhdsWithin` `IsClosed.smul` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `Mathlib.Tactic.Contrapose.contrapose₄` `mul_inv_rev` `inv_inv` `inv_mul_cancel_right` `lt_irrefl` `LE.le.trans_lt` `Eq.le` `Set.mem_iInter` `Set.Subset.antisymm` `Set.subset_iInter_iff` `Set.subset_mul_right` `Set.iInter_congr_Prop` `IsGδ.iInter_of_isOpen` `instCountableNat` `isOpen_biInter_finset`
`of_forall_exists_nhds_eq` 📖	—	`MeasureTheory.Measure.IsEverywherePos` `Set` `Filter` `Filter.instMembership` `nhds` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—	`lt_imp_lt_of_le_of_le` `le_refl` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_left` `Set.inter_subset_right` `Filter.inter_mem` `mem_nhdsWithin_of_mem_nhds`
`smul_measure` 📖	mathematical	`MeasureTheory.Measure.IsEverywherePos`	`ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instNoZeroDivisors` `bot_eq_zero'` `Ne.bot_lt`
`smul_measure_nnreal` 📖	mathematical	`MeasureTheory.Measure.IsEverywherePos`	`NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`smul_measure`

---

← Back to Index