BoundedVariation

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

Statistics

Metric	Count
Definitions `BoundedVariationOn`, `LocallyBoundedVariationOn`, `eVariationOn`, `variationOnFromTo`	4
Theorems `continuousWithinAt_leftLim`, `continuousWithinAt_rightLim`, `continuousWithinAt_variationOnFromTo_Ici`, `continuousWithinAt_variationOnFromTo_rightLim_Ici`, `dist_le`, `exists_tendsto_atBot`, `exists_tendsto_atTop`, `exists_tendsto_left`, `exists_tendsto_left_of_filter`, `exists_tendsto_right`, `leftLim`, `locallyBoundedVariationOn`, `mono`, `ofDual`, `rightLim`, `sub_le`, `tendsto_atBot_limUnder`, `tendsto_atTop_limUnder`, `tendsto_eVariationOn_Icc_zero_left`, `tendsto_eVariationOn_Icc_zero_right`, `tendsto_eVariationOn_Ici_zero`, `tendsto_eVariationOn_Ici_zero_of_filter`, `tendsto_eVariationOn_Ico_zero`, `tendsto_eVariationOn_Iic_zero`, `tendsto_eVariationOn_Ioc_zero`, `tendsto_leftLim`, `tendsto_rightLim`, `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`, `boundedVariation_ofDual`, `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`, `eVariationOn_eq_strictMonoOn`, `eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt`, `eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt`, `eVariationOn_leftLim_le`, `eVariationOn_rightLim_le`, `edist_le`, `eq_of_edist_zero_on`, `eq_of_eqOn`, `eq_zero_iff`, `exists_lt_eVariationOn_inter_Icc`, `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`, `abs_le_eVariationOn`, `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`	87
Total	91

BoundedVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousWithinAt_leftLim` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Function.leftLim` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tendsto_leftLim` `leftLim` `continuousWithinAt_Iio_iff_Iic` `leftLim_leftLim`
`continuousWithinAt_rightLim` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Function.rightLim` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`continuousWithinAt_leftLim` `instOrderTopologyOrderDual` `ofDual`
`continuousWithinAt_variationOnFromTo_Ici` 📖	mathematical	`BoundedVariationOn` `Set.univ` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `variationOnFromTo` `Set.univ` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`variationOnFromTo.add` `locallyBoundedVariationOn` `Set.mem_univ` `ContinuousWithinAt.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `continuousWithinAt_const` `Set.Icc_self` `eVariationOn.subsingleton` `Filter.Tendsto.comp` `ENNReal.tendsto_toReal` `ENNReal.zero_ne_top` `Filter.Tendsto.mono_left` `tendsto_eVariationOn_Icc_zero_right` `Set.univ_inter` `nhdsWithin_mono` `Set.subset_univ` `ContinuousWithinAt.congr_of_mem` `Set.self_mem_Iic`
`continuousWithinAt_variationOnFromTo_rightLim_Ici` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `variationOnFromTo` `Function.rightLim` `PseudoEMetricSpace.toUniformSpace` `Set.univ` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`continuousWithinAt_variationOnFromTo_Ici` `rightLim` `continuousWithinAt_rightLim`
`dist_le` 📖	mathematical	`BoundedVariationOn` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `ENNReal.toReal` `eVariationOn` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`ENNReal.ofReal_le_ofReal_iff` `ENNReal.toReal_nonneg` `ENNReal.ofReal_toReal` `edist_dist` `eVariationOn.edist_le`
`exists_tendsto_atBot` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `Filter` `Filter.instInf` `Filter.principal` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`exists_tendsto_atTop` `ofDual`
`exists_tendsto_atTop` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `Filter` `Filter.instInf` `Filter.principal` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Set.eq_empty_or_nonempty` `Filter.principal_empty` `inf_of_le_left` `exists_tendsto_left_of_filter` `Filter.inter_mem_inf` `Filter.mem_principal_self` `Filter.Ici_mem_atTop`
`exists_tendsto_left` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `nhdsWithin` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Set.eq_empty_or_nonempty` `nhdsWithin_empty` `exists_tendsto_left_of_filter` `mono` `Set.inter_subset_left` `inter_mem_nhdsWithin` `Ici_mem_nhds` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology`
`exists_tendsto_left_of_filter` 📖	mathematical	`BoundedVariationOn` `Set` `Filter` `Filter.instMembership` `Set.instInter` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Filter.eq_or_neBot` `CompleteSpace.complete` `EMetric.cauchy_iff` `Filter.neBot_iff` `tendsto_eVariationOn_Ici_zero_of_filter` `Filter.Eventually.exists` `Filter.Eventually.and` `tendsto_order` `ENNReal.instOrderTopology` `Filter.mem_of_superset` `Set.subset_preimage_image` `LE.le.trans_lt` `eVariationOn.edist_le`
`exists_tendsto_right` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `nhdsWithin` `Set` `Set.instInter` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`exists_tendsto_left` `instOrderTopologyOrderDual` `ofDual`
`leftLim` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`BoundedVariationOn` `Function.leftLim` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.univ`	—	`LT.lt.ne` `LE.le.trans_lt` `eVariationOn.eVariationOn_leftLim_le` `Ne.lt_top`
`locallyBoundedVariationOn` 📖	mathematical	`BoundedVariationOn`	`LocallyBoundedVariationOn`	—	`mono` `Set.inter_subset_left`
`mono` 📖	mathematical	`BoundedVariationOn` `Set` `Set.instHasSubset`	`BoundedVariationOn`	—	`ne_top_of_le_ne_top` `eVariationOn.mono`
`ofDual` 📖	mathematical	`BoundedVariationOn`	`BoundedVariationOn` `OrderDual` `OrderDual.instLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `Set.preimage`	—	`eVariationOn.comp_ofDual`
`rightLim` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`BoundedVariationOn` `Function.rightLim` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.univ`	—	`LT.lt.ne` `LE.le.trans_lt` `eVariationOn.eVariationOn_rightLim_le` `Ne.lt_top`
`sub_le` 📖	mathematical	`BoundedVariationOn` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set` `Set.instMembership`	`Real` `Real.instLE` `Real.instSub` `ENNReal.toReal` `eVariationOn` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	—	`LE.le.trans` `le_abs_self` `Real.dist_eq` `dist_le`
`tendsto_atBot_limUnder` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Filter.limUnder`	—	`tendsto_nhds_limUnder` `Filter.principal_univ` `inf_of_le_right` `exists_tendsto_atBot`
`tendsto_atTop_limUnder` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Filter.limUnder`	—	`tendsto_nhds_limUnder` `Filter.principal_univ` `inf_of_le_right` `exists_tendsto_atTop`
`tendsto_eVariationOn_Icc_zero_left` 📖	mathematical	`BoundedVariationOn` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhdsWithin` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Filter.eq_or_neBot` `Filter.Tendsto.congr'` `tendsto_const_nhds` `nhdsWithin_union` `sup_of_le_right` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `eVariationOn.subsingleton` `Filter.Tendsto.congr` `le_or_gt` `eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt` `nhdsWithin_inter_of_mem'` `mem_nhdsWithin_of_mem_nhds` `Ici_mem_nhds` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ContinuousWithinAt.mono` `tendsto_eVariationOn_Ico_zero`
`tendsto_eVariationOn_Icc_zero_right` 📖	mathematical	`BoundedVariationOn` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set` `Set.instInter` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhdsWithin` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Set.Icc_toDual` `Set.preimage_inter` `eVariationOn.comp_ofDual` `tendsto_eVariationOn_Icc_zero_left` `instOrderTopologyOrderDual` `ofDual`
`tendsto_eVariationOn_Ici_zero` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter` `Filter.instInf` `Filter.principal` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_eVariationOn_Ici_zero_of_filter` `Filter.inter_mem_inf` `Filter.mem_principal_self` `Filter.Ici_mem_atTop`
`tendsto_eVariationOn_Ici_zero_of_filter` 📖	mathematical	`BoundedVariationOn` `Set` `Filter` `Filter.instMembership` `Set.instInter` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Set.eq_empty_or_nonempty` `Set.empty_inter` `eVariationOn.subsingleton` `tendsto_const_nhds` `tendsto_order` `ENNReal.instOrderTopology` `ENNReal.instCanonicallyOrderedAdd` `instIsEmptyFalse` `exists_between` `ENNReal.instDenselyOrdered` `Filter.Frequently.exists` `Filter.Frequently.and_eventually` `eVariationOn.exists_lt_eVariationOn_inter_Icc` `LT.lt.trans_le` `le_trans` `LE.le.trans` `LT.lt.le` `Set.inter_assoc` `eVariationOn.mono` `Function.iterate_succ'` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `eVariationOn.sum` `monotone_nat_of_le_succ` `Set.inter_subset_left` `ENNReal.Tendsto.mul_const` `ENNReal.tendsto_nat_nhds_top` `le_of_tendsto` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ENNReal.top_mul` `LT.lt.ne'` `Filter.Eventually.of_forall` `le_antisymm` `le_top` `le_refl` `Function.sometimes_spec`
`tendsto_eVariationOn_Ico_zero` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhdsWithin` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_eVariationOn_Ici_zero_of_filter` `mono` `Set.inter_subset_left` `inter_mem_nhdsWithin` `Ici_mem_nhds` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Filter.Tendsto.congr'` `tendsto_const_nhds` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `Set.inter_empty` `eVariationOn.subsingleton` `nhdsWithin_union` `Filter.tendsto_sup`
`tendsto_eVariationOn_Iic_zero` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter` `Filter.instInf` `Filter.principal` `Filter.atBot` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Set.Ici_toDual` `Set.preimage_inter` `eVariationOn.comp_ofDual` `tendsto_eVariationOn_Ici_zero` `ofDual`
`tendsto_eVariationOn_Ioc_zero` 📖	mathematical	`BoundedVariationOn`	`Filter.Tendsto` `ENNReal` `eVariationOn` `Set` `Set.instInter` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhdsWithin` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Set.Ico_toDual` `Set.preimage_inter` `eVariationOn.comp_ofDual` `tendsto_eVariationOn_Ico_zero` `instOrderTopologyOrderDual` `ofDual`
`tendsto_leftLim` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Function.leftLim`	—	`tendsto_leftLim_of_tendsto` `Set.univ_inter` `exists_tendsto_left`
`tendsto_rightLim` 📖	mathematical	`BoundedVariationOn` `Set.univ`	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Function.rightLim`	—	`tendsto_leftLim` `instOrderTopologyOrderDual` `ofDual`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_boundedVariationOn` 📖	mathematical	`LipschitzOnWith` `Set.MapsTo` `BoundedVariationOn`	`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` 📖	mathematical	`LipschitzOnWith` `Set.MapsTo` `LocallyBoundedVariationOn`	`LocallyBoundedVariationOn`	—	`comp_boundedVariationOn` `Set.MapsTo.mono_left` `Set.inter_subset_left`
`locallyBoundedVariationOn` 📖	mathematical	`LipschitzOnWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`LocallyBoundedVariationOn` `Real` `Real.linearOrder`	—	`comp_locallyBoundedVariationOn` `Set.mapsTo_id` `MonotoneOn.locallyBoundedVariationOn` `monotoneOn_id`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_boundedVariationOn` 📖	mathematical	`LipschitzWith` `BoundedVariationOn`	`BoundedVariationOn`	—	`LipschitzOnWith.comp_boundedVariationOn` `lipschitzOnWith` `Set.mapsTo_univ`
`comp_locallyBoundedVariationOn` 📖	mathematical	`LipschitzWith` `LocallyBoundedVariationOn`	`LocallyBoundedVariationOn`	—	`LipschitzOnWith.comp_locallyBoundedVariationOn` `lipschitzOnWith` `Set.mapsTo_univ`
`locallyBoundedVariationOn` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`LocallyBoundedVariationOn` `Real` `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` `Real` `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` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set` `Set.instInter` `Set.Icc` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `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` `Real` `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	8 math math: `eVariationOn.boundedVariation_ofDual`, `AbsolutelyContinuousOnInterval.boundedVariationOn`, `BoundedVariationOn.ofDual`, `BoundedVariationOn.leftLim`, `LipschitzWith.comp_boundedVariationOn`, `BoundedVariationOn.rightLim`, `LipschitzOnWith.comp_boundedVariationOn`, `BoundedVariationOn.mono`
`LocallyBoundedVariationOn` 📖	MathDef	8 math math: `LipschitzWith.locallyBoundedVariationOn`, `MonotoneOn.locallyBoundedVariationOn`, `LipschitzOnWith.comp_locallyBoundedVariationOn`, `BoundedVariationOn.locallyBoundedVariationOn`, `HasConstantSpeedOnWith.hasLocallyBoundedVariationOn`, `LipschitzWith.comp_locallyBoundedVariationOn`, `LipschitzOnWith.locallyBoundedVariationOn`, `hasConstantSpeedOnWith_iff_variationOnFromTo_eq`
`eVariationOn` 📖	CompOp	46 math math: `eVariationOn.sum_le_of_monotoneOn_Icc`, `BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter`, `eVariationOn.add_le_union`, `eVariationOn.sum'`, `variationOnFromTo.eq_of_ge`, `eVariationOn.eVariationOn_rightLim_le`, `eVariationOn.comp_inter_Icc_eq_of_monotoneOn`, `eVariationOn.lowerSemicontinuous_aux`, `eVariationOn.comp_eq_of_antitoneOn`, `LipschitzOnWith.comp_eVariationOn_le`, `eVariationOn.sum_le_of_monotoneOn_Iic`, `BoundedVariationOn.sub_le`, `eVariationOn.union`, `eVariationOn.congr`, `BoundedVariationOn.tendsto_eVariationOn_Icc_zero_right`, `eVariationOn.sum`, `eVariationOn.eq_of_eqOn`, `BoundedVariationOn.tendsto_eVariationOn_Iic_zero`, `eVariationOn.edist_le`, `eVariationOn.comp_le_of_antitoneOn`, `eVariationOn.sum_le`, `eVariationOn.mono`, `eVariationOn.eVariationOn_eq_strictMonoOn`, `eVariationOn.exists_lt_eVariationOn_inter_Icc`, `BoundedVariationOn.dist_le`, `variationOnFromTo.abs_le_eVariationOn`, `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`, `BoundedVariationOn.tendsto_eVariationOn_Icc_zero_left`, `BoundedVariationOn.tendsto_eVariationOn_Ico_zero`, `eVariationOn.Icc_add_Icc`, `eVariationOn.eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt`, `hasConstantSpeedOnWith_iff_ordered`, `eVariationOn.lowerSemicontinuous`, `BoundedVariationOn.tendsto_eVariationOn_Ioc_zero`, `eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt`, `BoundedVariationOn.tendsto_eVariationOn_Ici_zero`, `eVariationOn.eVariationOn_leftLim_le`, `eVariationOn.eq_zero_iff`
`variationOnFromTo` 📖	CompOp	22 math math: `variationOnFromTo.eq_of_ge`, `variationOnFromTo.antitoneOn`, `BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici`, `variationOnFromTo.eq_zero_iff_of_le`, `BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici`, `variationOnFromTo.comp_eq_of_monotoneOn`, `variationOnFromTo.eq_zero_iff_of_ge`, `BoundedVariationOn.stieltjesFunctionRightLim_apply`, `variationOnFromTo.sub_self_monotoneOn`, `variationOnFromTo.add`, `variationOnFromTo.nonneg_of_le`, `variationOnFromTo.abs_le_eVariationOn`, `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` `Set.instInter` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`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` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `eVariationOn` `Set` `Set.instUnion`	—	`subsingleton` `zero_add` `Set.empty_union` `instReflLe` `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`	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership` `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`
`boundedVariation_ofDual` 📖	mathematical	—	`BoundedVariationOn` `OrderDual` `OrderDual.instLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `Set.preimage`	—	`BoundedVariationOn.ofDual`
`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` `Set.instInter` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `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` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `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`
`eVariationOn_eq_strictMonoOn` 📖	mathematical	—	`eVariationOn` `iSup` `ENNReal` `StrictMonoOn` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iic` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.range` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`le_antisymm` `iSup_le` `Finset.sum_congr` `Finset.sum_range_succ` `LE.le.eq_or_lt` `PseudoEMetricSpace.edist_self` `add_zero` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Nat.instNoMaxOrder` `le_iSup` `sum_le_of_monotoneOn_Iic`
`eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt` 📖	mathematical	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`eVariationOn` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iic`	—	`le_antisymm` `mono` `eVariationOn_eq_strictMonoOn` `iSup_le` `instReflLe` `LE.le.eq_or_lt` `Finset.sum_congr` `ENNReal.instCanonicallyOrderedAdd` `Finset.range_add_one` `Finset.sum_insert` `Filter.Tendsto.add_const` `instSeparatelyContinuousAddOfContinuousAdd` `ENNReal.instContinuousAdd` `Filter.Tendsto.edist` `Filter.Tendsto.mono_left` `ContinuousWithinAt.tendsto` `nhdsWithin_mono` `tendsto_const_nhds` `le_of_tendsto` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `inter_mem_nhdsWithin_inter` `self_mem_nhdsWithin` `Ioo_mem_nhdsLT` `Filter.mp_mem` `Filter.univ_mem'` `sum_le_of_monotoneOn_Iic` `StrictMonoOn.monotoneOn`
`eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt` 📖	mathematical	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set` `Set.instInter` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`eVariationOn` `Set` `Set.instInter` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici`	—	`comp_ofDual` `eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt` `instOrderTopologyOrderDual`
`eVariationOn_leftLim_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn` `Function.leftLim` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.univ`	—	`MapClusterPt.mono` `mapClusterPt_leftLim` `nhdsWithin_mono` `Set.subset_univ`
`eVariationOn_rightLim_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn` `Function.rightLim` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.univ`	—	`MapClusterPt.mono` `mapClusterPt_rightLim` `nhdsWithin_mono` `Set.subset_univ`
`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`
`exists_lt_eVariationOn_inter_Icc` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn`	`Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ENNReal` `ENNReal.instPartialOrder` `eVariationOn` `Set.instInter` `Set.Icc`	—	`Finset.sum_congr` `LT.lt.trans_le` `sum_le_of_monotoneOn_Iic` `le_antisymm` `le_trans` `le_refl` `subsingleton` `ENNReal.instCanonicallyOrderedAdd`
`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` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eVariationOn`	—	`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` `Set.instInter` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`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` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `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` `PartialOrder.toPreorder` `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
`abs_le_eVariationOn` 📖	mathematical	`BoundedVariationOn`	`Real` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `variationOnFromTo` `ENNReal.toReal` `eVariationOn`	—	`ENNReal.abs_toReal` `ENNReal.toReal_mono` `eVariationOn.mono` `Set.inter_subset_left` `abs_neg`
`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` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid`
`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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`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` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `Pi.instSub` `Real.instSub` `variationOnFromTo` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	—	`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