BoundedVariation

📁 Source: Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Statistics

Metric	Count
Definitions `BoundedVariationOn`, `LocallyBoundedVariationOn`, `eVariationOn`, `variationOnFromTo`	4
Theorems `dist_le`, `locallyBoundedVariationOn`, `mono`, `sub_le`, `comp_boundedVariationOn`, `comp_eVariationOn_le`, `comp_locallyBoundedVariationOn`, `locallyBoundedVariationOn`, `comp_boundedVariationOn`, `comp_locallyBoundedVariationOn`, `locallyBoundedVariationOn`, `exists_monotoneOn_sub_monotoneOn`, `eVariationOn_le`, `locallyBoundedVariationOn`, `Icc_add_Icc`, `add_le_union`, `add_point`, `comp_eq_of_antitoneOn`, `comp_eq_of_monotoneOn`, `comp_inter_Icc_eq_of_monotoneOn`, `comp_le_of_antitoneOn`, `comp_le_of_monotoneOn`, `comp_ofDual`, `constant_on`, `edist_le`, `eq_of_edist_zero_on`, `eq_of_eqOn`, `eq_zero_iff`, `lowerSemicontinuous`, `lowerSemicontinuous_aux`, `lowerSemicontinuous_uniformOn`, `mono`, `nonempty_monotone_mem`, `subsingleton`, `sum`, `sum'`, `sum_le`, `sum_le_of_monotoneOn_Icc`, `sum_le_of_monotoneOn_Iic`, `union`, `add`, `antitoneOn`, `comp_eq_of_monotoneOn`, `edist_zero_of_eq_zero`, `eq_left_iff`, `eq_neg_swap`, `eq_of_ge`, `eq_of_le`, `eq_zero_iff`, `eq_zero_iff_of_ge`, `eq_zero_iff_of_le`, `monotoneOn`, `nonneg_of_le`, `nonpos_of_ge`, `self`, `sub_self_monotoneOn`	56
Total	60

BoundedVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_le` 📖	mathematical	`BoundedVariationOn` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `ENNReal.toReal` `eVariationOn`	—	`ENNReal.ofReal_le_ofReal_iff` `ENNReal.toReal_nonneg` `ENNReal.ofReal_toReal` `edist_dist` `eVariationOn.edist_le`
`locallyBoundedVariationOn` 📖	mathematical	`BoundedVariationOn`	`LocallyBoundedVariationOn`	—	`mono` `Set.inter_subset_left`
`mono` 📖	—	`BoundedVariationOn` `Set` `Set.instHasSubset`	—	—	`ne_top_of_le_ne_top` `eVariationOn.mono`
`sub_le` 📖	mathematical	`BoundedVariationOn` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set` `Set.instMembership`	`Real.instLE` `Real.instSub` `ENNReal.toReal` `eVariationOn`	—	`LE.le.trans` `le_abs_self` `Real.dist_eq` `dist_le`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_boundedVariationOn` 📖	—	`LipschitzOnWith` `Set.MapsTo` `BoundedVariationOn`	—	—	`ne_top_of_le_ne_top` `ENNReal.mul_ne_top` `ENNReal.coe_ne_top` `comp_eVariationOn_le`
`comp_eVariationOn_le` 📖	mathematical	`LipschitzOnWith` `Set.MapsTo`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`iSup_le` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Finset.mul_sum` `le_imp_le_of_le_of_le` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `eVariationOn.sum_le` `le_refl`
`comp_locallyBoundedVariationOn` 📖	—	`LipschitzOnWith` `Set.MapsTo` `LocallyBoundedVariationOn`	—	—	`comp_boundedVariationOn` `Set.MapsTo.mono_left` `Set.inter_subset_left`
`locallyBoundedVariationOn` 📖	mathematical	`LipschitzOnWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`LocallyBoundedVariationOn` `Real.linearOrder`	—	`comp_locallyBoundedVariationOn` `Set.mapsTo_id` `MonotoneOn.locallyBoundedVariationOn` `monotoneOn_id`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_boundedVariationOn` 📖	—	`LipschitzWith` `BoundedVariationOn`	—	—	`LipschitzOnWith.comp_boundedVariationOn` `lipschitzOnWith` `Set.mapsTo_univ`
`comp_locallyBoundedVariationOn` 📖	—	`LipschitzWith` `LocallyBoundedVariationOn`	—	—	`LipschitzOnWith.comp_locallyBoundedVariationOn` `lipschitzOnWith` `Set.mapsTo_univ`
`locallyBoundedVariationOn` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`LocallyBoundedVariationOn` `Real.linearOrder`	—	`LipschitzOnWith.locallyBoundedVariationOn` `lipschitzOnWith`

LocallyBoundedVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_monotoneOn_sub_monotoneOn` 📖	mathematical	`LocallyBoundedVariationOn` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `Pi.instSub` `Real.instSub`	—	`Set.eq_empty_or_nonempty` `Set.Subsingleton.monotoneOn` `Set.subsingleton_empty` `sub_zero` `variationOnFromTo.monotoneOn` `variationOnFromTo.sub_self_monotoneOn` `sub_sub_cancel`

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eVariationOn_le` 📖	mathematical	`MonotoneOn` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `eVariationOn` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set.instInter` `Set.Icc` `ENNReal.ofReal` `Real.instSub`	—	`iSup_le` `Finset.sum_congr` `edist_dist` `Real.dist_eq` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `ENNReal.ofReal_sum_of_nonneg` `Finset.sum_range_sub` `ENNReal.ofReal_le_ofReal` `sub_le_sub`
`locallyBoundedVariationOn` 📖	mathematical	`MonotoneOn` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder`	`LocallyBoundedVariationOn` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	—	`LT.lt.ne` `LE.le.trans_lt` `eVariationOn_le` `ENNReal.ofReal_lt_top`

(root)

Definitions

Name	Category	Theorems
`BoundedVariationOn` 📖	MathDef	1 math math: `AbsolutelyContinuousOnInterval.boundedVariationOn`
`LocallyBoundedVariationOn` 📖	MathDef	6 math math: `LipschitzWith.locallyBoundedVariationOn`, `MonotoneOn.locallyBoundedVariationOn`, `BoundedVariationOn.locallyBoundedVariationOn`, `HasConstantSpeedOnWith.hasLocallyBoundedVariationOn`, `LipschitzOnWith.locallyBoundedVariationOn`, `hasConstantSpeedOnWith_iff_variationOnFromTo_eq`
`eVariationOn` 📖	CompOp	30 math math: `eVariationOn.sum_le_of_monotoneOn_Icc`, `eVariationOn.add_le_union`, `eVariationOn.sum'`, `variationOnFromTo.eq_of_ge`, `eVariationOn.comp_inter_Icc_eq_of_monotoneOn`, `eVariationOn.comp_eq_of_antitoneOn`, `LipschitzOnWith.comp_eVariationOn_le`, `eVariationOn.sum_le_of_monotoneOn_Iic`, `BoundedVariationOn.sub_le`, `eVariationOn.union`, `eVariationOn.sum`, `eVariationOn.eq_of_eqOn`, `eVariationOn.edist_le`, `eVariationOn.comp_le_of_antitoneOn`, `eVariationOn.sum_le`, `eVariationOn.mono`, `BoundedVariationOn.dist_le`, `eVariationOn.comp_le_of_monotoneOn`, `eVariationOn.lowerSemicontinuous_uniformOn`, `eVariationOn.comp_ofDual`, `variationOnFromTo.eq_of_le`, `eVariationOn.comp_eq_of_monotoneOn`, `eVariationOn.constant_on`, `eVariationOn.subsingleton`, `eVariationOn.eq_of_edist_zero_on`, `MonotoneOn.eVariationOn_le`, `eVariationOn.Icc_add_Icc`, `hasConstantSpeedOnWith_iff_ordered`, `eVariationOn.lowerSemicontinuous`, `eVariationOn.eq_zero_iff`
`variationOnFromTo` 📖	CompOp	18 math math: `variationOnFromTo.eq_of_ge`, `variationOnFromTo.antitoneOn`, `variationOnFromTo.eq_zero_iff_of_le`, `variationOnFromTo.comp_eq_of_monotoneOn`, `variationOnFromTo.eq_zero_iff_of_ge`, `variationOnFromTo.sub_self_monotoneOn`, `variationOnFromTo.add`, `variationOnFromTo.nonneg_of_le`, `variationOnFromTo.nonpos_of_ge`, `variationOnFromTo.monotoneOn`, `variationOnFromTo.eq_of_le`, `variationOnFromTo.eq_zero_iff`, `variationOnFromTo.eq_left_iff`, `variationOnFromTo.eq_neg_swap`, `has_unit_speed_naturalParameterization`, `variationOnFromTo.self`, `hasConstantSpeedOnWith_iff_variationOnFromTo_eq`, `edist_naturalParameterization_eq_zero`

eVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_add_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `eVariationOn` `Set.instInter` `Set.Icc`	—	`le_rfl` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `Set.Icc_subset_Iic_self` `Set.Icc_subset_Ici_self` `union` `Set.inter_union_distrib_left` `Set.Icc_union_Icc_eq_Icc`
`add_le_union` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`ENNReal` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `eVariationOn` `Set` `Set.instUnion`	—	`subsingleton` `zero_add` `Set.empty_union` `nonempty_monotone_mem` `Set.nonempty_iff_ne_empty` `add_zero` `Set.union_empty` `ENNReal.iSup_add_iSup_le` `Finset.range_eq_Ico` `Finset.sum_congr` `Mathlib.Tactic.Abel.subst_into_add` `Mathlib.Tactic.Abel.term_atom` `Mathlib.Tactic.Abel.term_add_const` `Mathlib.Tactic.Abel.const_add_term` `Finset.sum_Ico_add` `Nat.instIsOrderedCancelAddMonoid` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Finset.sum_union` `Finset.disjoint_left` `Finset.sum_le_sum_of_subset_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `sum_le`
`add_point` 📖	mathematical	`Set` `Set.instMembership` `Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.image` `Set.Iio` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.range` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`le_or_gt` `Set.mem_image` `Finset.sum_le_sum_of_subset_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `le_rfl` `Nat.find_spec` `monotone_nat_of_le_succ` `lt_trichotomy` `Nat.find_min` `eq_or_lt_of_le` `Nat.instCanonicallyOrderedAdd` `Finset.range_eq_Ico` `Finset.sum_Ico_add` `Nat.instIsOrderedCancelAddMonoid` `CanonicallyOrderedAdd.toExistsAddOfLE` `Finset.Ico_subset_Ico` `zero_le_one` `Nat.instZeroLEOneClass` `le_refl` `Finset.sum_Ico_consecutive` `Nat.Ico_succ_singleton` `Finset.sum_congr` `Finset.sum_singleton` `add_le_add` `covariant_swap_add_of_covariant_add` `lt_of_le_of_lt` `Finset.sum_eq_sum_Ico_succ_bot` `Finset.Ico_self` `Finset.sum_empty` `add_zero` `add_comm` `PseudoEMetricSpace.edist_triangle`
`comp_eq_of_antitoneOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`eVariationOn` `Set.image`	—	`le_antisymm` `comp_le_of_antitoneOn` `Set.mapsTo_image` `isEmpty_or_nonempty` `subsingleton` `Set.Subsingleton.anti` `Set.Subsingleton.image` `Set.subsingleton_of_subsingleton` `IsEmpty.instSubsingleton` `Set.surjOn_image` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `Set.SurjOn.rightInvOn_invFunOn` `Set.SurjOn.mapsTo_invFunOn` `Function.antitoneOn_of_rightInvOn_of_mapsTo` `eq_of_eqOn` `Set.EqOn.comp_left`
`comp_eq_of_monotoneOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`eVariationOn` `Set.image`	—	`le_antisymm` `comp_le_of_monotoneOn` `Set.mapsTo_image` `isEmpty_or_nonempty` `subsingleton` `Set.Subsingleton.anti` `Set.Subsingleton.image` `Set.subsingleton_of_subsingleton` `IsEmpty.instSubsingleton` `Set.surjOn_image` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `Set.SurjOn.rightInvOn_invFunOn` `Set.SurjOn.mapsTo_invFunOn` `Function.monotoneOn_of_rightInvOn_of_mapsTo` `eq_of_eqOn` `Set.EqOn.comp_left`
`comp_inter_Icc_eq_of_monotoneOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`eVariationOn` `Set.instInter` `Set.Icc` `Set.image`	—	`le_total` `le_antisymm` `le_rfl` `comp_eq_of_monotoneOn` `MonotoneOn.mono` `Set.inter_subset_left` `subsingleton` `Set.Subsingleton.anti` `Set.subsingleton_Icc_of_ge` `Set.inter_subset_right`
`comp_le_of_antitoneOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.MapsTo`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `eVariationOn`	—	`iSup_le` `Finset.sum_range_reflect` `Eq.trans_le` `Finset.sum_congr` `PseudoEMetricSpace.edist_comm` `Finset.mem_range` `le_iSup_of_le` `le_rfl`
`comp_le_of_monotoneOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.MapsTo`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `eVariationOn`	—	`iSup_le` `le_iSup_of_le` `le_rfl`
`comp_ofDual` 📖	mathematical	—	`eVariationOn` `OrderDual` `OrderDual.instLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `Set.preimage`	—	`Equiv.image_preimage` `comp_eq_of_antitoneOn`
`constant_on` 📖	mathematical	`Set.Subsingleton` `Set.image`	`eVariationOn` `ENNReal` `instZeroENNReal`	—	`eq_zero_iff` `PseudoEMetricSpace.edist_self`
`edist_le` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `eVariationOn`	—	`monotone_nat_of_le_succ` `le_rfl` `Finset.sum_range_one` `sum_le` `PseudoEMetricSpace.edist_comm` `le_of_not_ge`
`eq_of_edist_zero_on` 📖	mathematical	`EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal`	`eVariationOn`	—	`edist_congr_right` `Subtype.prop` `edist_congr_left`
`eq_of_eqOn` 📖	mathematical	`Set.EqOn`	`eVariationOn`	—	`eq_of_edist_zero_on` `PseudoEMetricSpace.edist_self`
`eq_zero_iff` 📖	mathematical	—	`eVariationOn` `ENNReal` `instZeroENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `edist_le` `ENNReal.iSup_eq_zero` `Finset.sum_eq_zero`
`lowerSemicontinuous` 📖	mathematical	—	`LowerSemicontinuous` `UniformOnFun` `Set.image` `Set` `Set.instSingletonSet` `ENNReal` `UniformOnFun.topologicalSpace` `PseudoEMetricSpace.toUniformSpace` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn`	—	`lowerSemicontinuous_aux` `Filter.tendsto_id`
`lowerSemicontinuous_aux` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn`	`Filter.Eventually`	—	`lt_iSup_iff` `tendsto_finset_sum` `ENNReal.instContinuousAdd` `Filter.Tendsto.edist` `Filter.Eventually.mono` `Filter.Tendsto.eventually_const_lt` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `LT.lt.trans_le` `sum_le`
`lowerSemicontinuous_uniformOn` 📖	mathematical	—	`LowerSemicontinuous` `UniformOnFun` `Set` `Set.instSingletonSet` `ENNReal` `UniformOnFun.topologicalSpace` `PseudoEMetricSpace.toUniformSpace` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn`	—	`lowerSemicontinuous_aux` `Filter.tendsto_id` `TendstoUniformlyOn.mono` `UniformOnFun.tendsto_iff_tendstoUniformlyOn` `Set.singleton_subset_iff`
`mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn`	—	`iSup_le` `sum_le`
`nonempty_monotone_mem` 📖	mathematical	`Set.Nonempty`	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_rfl`
`subsingleton` 📖	mathematical	`Set.Subsingleton`	`eVariationOn` `ENNReal` `instZeroENNReal`	—	`constant_on` `Set.Subsingleton.image`
`sum` 📖	mathematical	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.range` `eVariationOn` `Set.instInter` `Set.Icc`	—	`Set.Icc_self` `subsingleton` `Set.Subsingleton.inter_singleton` `Finset.sum_congr` `zero_add` `Finset.sum_singleton` `Icc_add_Icc` `Finset.sum_range_succ`
`sum'` 📖	mathematical	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.range` `eVariationOn` `Set.Icc`	—	`Finset.sum_congr` `Set.Icc_subset_Icc` `Finset.mem_range` `Set.inter_self` `sum` `Set.mem_Icc`
`sum_le` 📖	mathematical	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.range` `EDist.edist` `PseudoEMetricSpace.toEDist` `eVariationOn`	—	`le_iSup_of_le` `le_rfl`
`sum_le_of_monotoneOn_Icc` 📖	mathematical	`MonotoneOn` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc` `Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.Ico` `Nat.instLocallyFiniteOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `eVariationOn`	—	`le_total` `Finset.sum_congr` `Finset.Ico_eq_empty_of_le` `ENNReal.instCanonicallyOrderedAdd` `LE.le.trans` `Finset.mem_Ico` `Set.projIcc_of_mem` `LT.lt.le` `Finset.sum_mono_set` `Finset.Ico_subset_Iio_self` `Nat.Iio_eq_range` `sum_le` `Set.monotone_projIcc`
`sum_le_of_monotoneOn_Iic` 📖	mathematical	`MonotoneOn` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iic` `Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.range` `EDist.edist` `PseudoEMetricSpace.toEDist` `eVariationOn`	—	`Finset.sum_congr` `Nat.Ico_zero_eq_range` `sum_le_of_monotoneOn_Icc` `MonotoneOn.mono` `Set.Icc_subset_Iic_self`
`union` 📖	mathematical	`IsGreatest` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsLeast`	`eVariationOn` `Set` `Set.instUnion` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`le_antisymm` `iSup_le` `add_point` `Set.mem_union_left` `Finset.range_eq_Ico` `Finset.sum_Ico_consecutive` `zero_le` `Nat.instCanonicallyOrderedAdd` `LT.lt.le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `sum_le_of_monotoneOn_Icc` `Monotone.monotoneOn` `add_le_union` `le_trans`

variationOnFromTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership`	`Real` `Real.instAdd` `variationOnFromTo`	—	`additive_of_total` `LE.total` `eq_neg_swap` `add_neg_cancel` `eq_of_le` `LE.le.trans` `ENNReal.toReal_add` `eVariationOn.Icc_add_Icc`
`antitoneOn` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership`	`AntitoneOn` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `variationOnFromTo`	—	`add` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `nonneg_of_le`
`comp_eq_of_monotoneOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`variationOnFromTo` `Set.image`	—	`le_total` `eq_of_le` `eVariationOn.comp_inter_Icc_eq_of_monotoneOn` `eq_of_ge`
`edist_zero_of_eq_zero` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership` `variationOnFromTo` `Real` `Real.instZero`	`EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal`	—	`le_antisymm` `ENNReal.ofReal_zero` `eq_of_le` `ENNReal.ofReal_toReal` `eVariationOn.edist_le` `le_rfl` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `PseudoEMetricSpace.edist_comm` `eq_neg_swap` `neg_zero` `le_of_not_ge`
`eq_left_iff` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership`	`variationOnFromTo` `Real` `Real.instZero`	—	`add` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`eq_neg_swap` 📖	mathematical	—	`variationOnFromTo` `Real` `Real.instNeg`	—	`lt_trichotomy` `LT.lt.le` `LT.lt.not_ge` `neg_neg` `self` `neg_zero`
`eq_of_ge` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`variationOnFromTo` `Real` `Real.instNeg` `ENNReal.toReal` `eVariationOn` `Set` `Set.instInter` `Set.Icc`	—	`eq_neg_swap` `eq_of_le`
`eq_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`variationOnFromTo` `ENNReal.toReal` `eVariationOn` `Set` `Set.instInter` `Set.Icc`	—	—
`eq_zero_iff` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership`	`variationOnFromTo` `Real` `Real.instZero` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal`	—	`le_total` `Set.uIcc_of_le` `eq_zero_iff_of_le` `Set.uIcc_of_ge` `eq_zero_iff_of_ge`
`eq_zero_iff_of_ge` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`variationOnFromTo` `Real` `Real.instZero` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal`	—	`eq_of_ge` `neg_eq_zero` `ENNReal.toReal_eq_zero_iff` `eVariationOn.eq_zero_iff`
`eq_zero_iff_of_le` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`variationOnFromTo` `Real` `Real.instZero` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal`	—	`eq_of_le` `ENNReal.toReal_eq_zero_iff` `eVariationOn.eq_zero_iff`
`monotoneOn` 📖	mathematical	`LocallyBoundedVariationOn` `Set` `Set.instMembership`	`MonotoneOn` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `variationOnFromTo`	—	`add` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `nonneg_of_le`
`nonneg_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Real` `Real.instLE` `Real.instZero` `variationOnFromTo`	—	—
`nonpos_of_ge` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Real` `Real.instLE` `variationOnFromTo` `Real.instZero`	—	`eq_neg_swap` `neg_nonpos_of_nonneg` `Real.instIsOrderedAddMonoid` `nonneg_of_le`
`self` 📖	mathematical	—	`variationOnFromTo` `Real` `Real.instZero`	—	`le_rfl` `Set.Icc_self` `eVariationOn.subsingleton` `ENNReal.toReal_zero`
`sub_self_monotoneOn` 📖	mathematical	`LocallyBoundedVariationOn` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set` `Set.instMembership`	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `Pi.instSub` `Real.instSub` `variationOnFromTo`	—	`Pi.sub_apply` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_comm_sub` `le_sub_iff_add_le'` `le_abs_self` `dist_comm` `Real.dist_eq` `eq_of_le` `dist_edist` `ENNReal.toReal_mono` `eVariationOn.edist_le` `le_rfl` `add` `add_sub_cancel_left`

---

← Back to Index