LiminfLimsup

📁 Source: Mathlib/MeasureTheory/Covering/LiminfLimsup.lean

Statistics

Metric	Count
Definitions	0
Theorems blimsup_cthickening_ae_eq_blimsup_thickening, blimsup_cthickening_ae_le_of_eventually_mul_le, blimsup_cthickening_ae_le_of_eventually_mul_le_aux, blimsup_cthickening_mul_ae_eq, blimsup_thickening_mul_ae_eq, blimsup_thickening_mul_ae_eq_aux	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
blimsup_cthickening_ae_eq_blimsup_thickening 📖	mathematical	Filter.Tendsto Real Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.Eventually	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.blimsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Metric.cthickening PseudoMetricSpace.toPseudoEMetricSpace Metric.thickening	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyLE_antisymm_iff Nat.instAtLeastTwoHAddOfNat Filter.eventuallyLE_congr Filter.EventuallyEq.symm blimsup_cthickening_mul_ae_eq one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.EventuallyEq.rfl HasSubset.Subset.eventuallyLE Filter.mono_blimsup' Filter.Eventually.mono Metric.cthickening_subset_thickening' lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_neg_of_lt Filter.mono_blimsup Metric.thickening_subset_cthickening
blimsup_cthickening_ae_le_of_eventually_mul_le 📖	mathematical	Real Real.instLT Real.instZero Filter.Tendsto Filter.atTop Nat.instPreorder nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder Filter.Eventually Real.instLE Real.instMul	Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.blimsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Metric.cthickening PseudoMetricSpace.toPseudoEMetricSpace	—	le_max_left Filter.Eventually.mono mul_max_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le MulZeroClass.mul_zero max_le_max le_refl MeasureTheory.Measure.instOuterMeasureClass Metric.cthickening_max_zero le_or_gt HasSubset.Subset.eventuallyLE Filter.mono_blimsup' Metric.cthickening_mono LE.le.trans le_mul_of_one_le_left IsOrderedRing.toMulPosMono Metric.cthickening_closure isClosed_closure blimsup_cthickening_ae_le_of_eventually_mul_le_aux Filter.tendsto_nhds_max_right HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
blimsup_cthickening_ae_le_of_eventually_mul_le_aux 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Filter.Tendsto Real Filter.atTop Nat.instPreorder nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder Pi.hasLe Real.instLE Pi.instZero Real.instLT Real.instOne Filter.Eventually Real.instMul	Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.blimsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Metric.cthickening PseudoMetricSpace.toPseudoEMetricSpace	—	MeasureTheory.Measure.instOuterMeasureClass Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div Set.mem_diff Filter.exists_forall_mem_of_hasBasis_mem_blimsup' Filter.atTop_basis instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.tendsto_atTop_atTop LE.le.trans Filter.Tendsto.comp Filter.Tendsto.eventually eq_or_lt_of_le Pi.zero_apply IsClosed.closure_eq Metric.cthickening_zero MulZeroClass.mul_zero dist_self Set.mem_iUnion₂ Metric.cthickening_subset_iUnion_closedBall_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_two_mul_self Real.instZeroLEOneClass IsStrictOrderedRing.toMulPosStrictMono NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_of_lt_of_le zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing IsUnifLocDoublingMeasure.one_le_scalingConstantOf tsub_lt_self NNReal.instCanonicallyOrderedAdd NNReal.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT NNReal.addLeftReflectLT inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono ne_of_gt Metric.closedBall_subset_closedBall mul_le_of_le_one_left IsOrderedRing.toMulPosMono LT.lt.le Set.inter_subset_right Filter.Eventually.mp Filter.eventually_atTop Disjoint.inf_right Disjoint.inf_right' Set.disjoint_compl_right_iff_subset HasSubset.Subset.trans Set.instIsTransSubset Metric.closedBall_subset_cthickening Metric.cthickening_mono GE.ge.le Filter.Eventually.mono IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul' Filter.Eventually.and eq_or_ne ENNReal.div_top ENNReal.coe_sub ENNReal.instCanonicallyOrderedAdd ENNReal.div_le_of_le_mul ENNReal.coe_one ENNReal.sub_mul one_mul ENNReal.mul_ne_top ENNReal.coe_ne_top ENNReal.coe_inv ENNReal.div_eq_inv_mul ENNReal.div_le_of_le_mul' le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add ENNReal.instIsOrderedAddMonoid le_refl MeasureTheory.measure_union' measurableSet_closedBall BorelSpace.opensMeasurable MeasureTheory.measure_mono Set.union_subset tsub_le_tsub_right ENNReal.instOrderedSub ENNReal.add_sub_cancel_left le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot Filter.Eventually.of_forall lt_self_iff_false MeasureTheory.ae_le_set Filter.blimsup_eq_iInf_biSup_of_nat Set.iInf_eq_iInter Set.diff_iInter MeasureTheory.measure_iUnion_null_iff instCountableNat
blimsup_cthickening_mul_ae_eq 📖	mathematical	Real Real.instLT Real.instZero Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.blimsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Metric.cthickening PseudoMetricSpace.toPseudoEMetricSpace Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass MulZeroClass.mul_zero Filter.TendstoNhdsWithinIoi.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.eventuallyLE_antisymm_iff blimsup_cthickening_ae_le_of_eventually_mul_le inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Filter.Eventually.of_forall inv_mul_cancel_left₀ LT.lt.ne' le_refl tendsto_nhdsWithin_iff Filter.Tendsto.if' tendsto_one_div_add_atTop_nhds_zero_nat RCLike.charZero_rclike NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal one_div Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono LT.lt.le Metric.cthickening_of_nonpos lt_or_ge Filter.blimsup_or_eq_sup Filter.blimsup_congr MeasureTheory.ae_eq_set_union MeasureTheory.ae_eq_refl
blimsup_thickening_mul_ae_eq 📖	mathematical	Real Real.instLT Real.instZero Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.blimsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Metric.thickening PseudoMetricSpace.toPseudoEMetricSpace Real.instMul	—	Filter.blimsup_congr' Filter.Eventually.of_forall Mathlib.Tactic.Contrapose.contrapose₂ Metric.thickening_of_nonpos mul_pos_iff_of_pos_left IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE MeasureTheory.Measure.instOuterMeasureClass blimsup_thickening_mul_ae_eq_aux
blimsup_thickening_mul_ae_eq_aux 📖	mathematical	Real Real.instLT Real.instZero Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.blimsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Metric.thickening PseudoMetricSpace.toPseudoEMetricSpace Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass blimsup_cthickening_ae_eq_blimsup_thickening blimsup_cthickening_mul_ae_eq MulZeroClass.mul_zero Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Eventually.mono mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Filter.EventuallyEq.trans Filter.EventuallyEq.symm

---

← Back to Index