BoundedVariation

📁 Source: Mathlib/MeasureTheory/VectorMeasure/BoundedVariation.lean

Statistics

Metric	Count
Definitions stieltjesFunctionRightLim, vectorMeasure	2
Theorems stieltjesFunctionRightLim_apply, vectorMeasure_Icc, vectorMeasure_Ici, vectorMeasure_Ico, vectorMeasure_Iic, vectorMeasure_Iio, vectorMeasure_Ioc, vectorMeasure_Ioi, vectorMeasure_Ioo, vectorMeasure_singleton, vectorMeasure_univ	11
Total	13

BoundedVariationOn

Definitions

Name	Category	Theorems
stieltjesFunctionRightLim 📖	CompOp	1 math math: stieltjesFunctionRightLim_apply
vectorMeasure 📖	CompOp	10 math math: vectorMeasure_univ, vectorMeasure_Iic, vectorMeasure_Icc, vectorMeasure_Ioi, vectorMeasure_Iio, vectorMeasure_singleton, vectorMeasure_Ici, vectorMeasure_Ioo, vectorMeasure_Ico, vectorMeasure_Ioc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stieltjesFunctionRightLim_apply 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	StieltjesFunction.toFun stieltjesFunctionRightLim variationOnFromTo EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Function.rightLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.univ	—	—
vectorMeasure_Icc 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.rightLim Function.leftLim	—	Set.Icc_union_Ioc_eq_Icc le_rfl MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Icc_self measurableSet_Icc BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology measurableSet_Ioc instClosedIicTopology vectorMeasure_singleton vectorMeasure_Ioc sub_add_sub_cancel'
vectorMeasure_Ici 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Filter.limUnder AddTorsor.nonempty addGroupIsAddTorsor Filter.atTop Function.leftLim	—	AddTorsor.nonempty tendsto_atTop_limUnder Filter.exists_seq_monotone_tendsto_atTop_atTop SemilatticeSup.instIsDirectedOrder instIsCountablyGenerated_atTop TopologicalSpace.SecondCountableTopology.to_separableSpace le_antisymm Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually Filter.Ici_mem_atTop MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace measurableSet_Icc BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology Filter.mp_mem Filter.univ_mem' vectorMeasure_Icc Filter.Tendsto.congr' Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.comp tendsto_rightLim_atTop_of_tendsto T4Space.t3Space instT4SpaceOfMetrizableSpace tendsto_const_nhds tendsto_nhds_unique
vectorMeasure_Ico 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.leftLim	—	LE.le.eq_or_lt Set.Ico_eq_empty MeasureTheory.VectorMeasure.empty sub_self Set.Icc_union_Ioo_eq_Ico le_rfl MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Icc_self measurableSet_Icc BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology measurableSet_Ioo vectorMeasure_Icc vectorMeasure_Ioo Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg
vectorMeasure_Iic 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.rightLim Filter.limUnder AddTorsor.nonempty addGroupIsAddTorsor Filter.atBot	—	AddTorsor.nonempty tendsto_atBot_limUnder Filter.exists_seq_antitone_tendsto_atTop_atBot SemilatticeInf.instIsCodirectedOrder instIsCountablyGenerated_atBot TopologicalSpace.SecondCountableTopology.to_separableSpace le_antisymm Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually Filter.Iic_mem_atBot MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace measurableSet_Icc BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology Filter.mp_mem Filter.univ_mem' vectorMeasure_Icc Filter.Tendsto.congr' Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_const_nhds Filter.Tendsto.comp tendsto_leftLim_atBot_of_tendsto T4Space.t3Space instT4SpaceOfMetrizableSpace tendsto_nhds_unique
vectorMeasure_Iio 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.leftLim Filter.limUnder AddTorsor.nonempty addGroupIsAddTorsor Filter.atBot	—	AddTorsor.nonempty vectorMeasure_Iic vectorMeasure_Icc le_rfl MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Icc_self measurableSet_Iio BorelSpace.opensMeasurable instClosedIciTopology OrderTopology.to_orderClosedTopology measurableSet_Icc Set.Iio_union_Icc_eq_Iic
vectorMeasure_Ioc 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.rightLim	—	MeasureTheory.VectorMeasure.dirac_apply_of_notMem add_zero
vectorMeasure_Ioi 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Filter.limUnder AddTorsor.nonempty addGroupIsAddTorsor Filter.atTop Function.rightLim	—	AddTorsor.nonempty vectorMeasure_Ici vectorMeasure_Icc le_rfl MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Icc_self measurableSet_Icc BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology measurableSet_Ioi instClosedIicTopology Set.Icc_union_Ioi_eq_Ici
vectorMeasure_Ioo 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.leftLim Function.rightLim	—	vectorMeasure_Ioc LT.lt.le vectorMeasure_Icc le_rfl MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.Icc_self measurableSet_Ioo BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology measurableSet_Icc Set.Ioo_union_Icc_eq_Ioc
vectorMeasure_singleton 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Function.rightLim Function.leftLim	—	Set.subsingleton_isBot botSet_eq_singleton_of_isBot zero_add MeasureTheory.VectorMeasure.dirac_apply_of_mem MeasurableSet.singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space leftLim_eq_of_isBot exists_seq_strictMono_tendsto' TopologicalSpace.SecondCountableTopology.to_firstCountableTopology Set.Subset.antisymm Set.mem_singleton_iff instReflLe le_of_tendsto' instClosedIicTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LT.lt.le le_antisymm MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Set.Ioc_subset_Ioc_left StrictMono.monotone measurableSet_Ioc vectorMeasure_Ioc Filter.Tendsto.sub tendsto_const_nhds tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within Filter.Eventually.of_forall mem_closure_iff_nhdsWithin_neBot closure_Iio' Set.self_mem_Iic leftLim_rightLim instT4SpaceOfMetrizableSpace tendsto_leftLim Filter.Tendsto.comp rightLim tendsto_nhds_unique
vectorMeasure_univ 📖	mathematical	BoundedVariationOn EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.univ	MeasureTheory.VectorMeasure.measureOf' AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup vectorMeasure Set.univ SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Filter.limUnder AddTorsor.nonempty addGroupIsAddTorsor Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atBot	—	AddTorsor.nonempty isEmpty_or_nonempty Set.eq_empty_of_isEmpty instIsEmptySubtype MeasureTheory.VectorMeasure.empty Filter.limUnder.congr_simp Filter.filter_eq_bot_of_isEmpty sub_self Set.Iio_union_Ici MeasureTheory.VectorMeasure.of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instReflLe measurableSet_Iio BorelSpace.opensMeasurable instClosedIciTopology OrderTopology.to_orderClosedTopology measurableSet_Ici vectorMeasure_Iio vectorMeasure_Ici Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg

---

← Back to Index