Lipschitz

📁 Source: Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean

Statistics

Metric	Count
Definitions	0
Theorems cauchySeq_comp, cauchySeq_comp, exists_lipschitzOnWith_of_compact, continuousAt_of_locally_lipschitz	4
Total	4

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_comp 📖	—	LipschitzOnWith PseudoMetricSpace.toPseudoEMetricSpace CauchySeq PseudoMetricSpace.toUniformSpace Nat.instPreorder Set Set.instHasSubset Set.range	—	—	cauchySeq_iff_le_tendsto_0 mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg Set.mem_range_self LE.le.trans dist_le_mul mul_le_mul_of_nonneg_left MulZeroClass.mul_zero Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing Real.instIsStrictOrderedRing instOrderTopologyReal

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_comp 📖	—	LipschitzWith PseudoMetricSpace.toPseudoEMetricSpace CauchySeq PseudoMetricSpace.toUniformSpace Nat.instPreorder	—	—	cauchySeq_iff_le_tendsto_0 mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg dist_le_mul_of_le MulZeroClass.mul_zero Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing Real.instIsStrictOrderedRing instOrderTopologyReal

LocallyLipschitzOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lipschitzOnWith_of_compact 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace LocallyLipschitzOn PseudoMetricSpace.toPseudoEMetricSpace	LipschitzOnWith	—	continuousOn Metric.mem_nhdsWithin_iff LipschitzOnWith.mono IsCompact.bddAbove_image instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal IsCompact.diff Metric.isOpen_ball ContinuousOn.div IsTopologicalDivisionRing.toContinuousInv₀ IsStrictOrderedRing.toIsTopologicalDivisionRing Real.instIsStrictOrderedRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing ContinuousOn.mono Continuous.comp_continuousOn' Continuous.dist continuous_const continuous_id' Set.diff_subset Continuous.continuousOn LT.lt.ne' LT.lt.trans_le not_lt dist_comm le_sup_right edist_nndist div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono NNReal.instIsStrictOrderedRing NNReal.coe_pos coe_nndist mem_upperBounds Set.mem_image_of_mem Nat.instAtLeastTwoHAddOfNat IsCompact.elim_nhdsWithin_subcover' inter_mem_nhdsWithin Metric.ball_mem_nhds half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Set.mem_iUnion₂ LE.le.trans LT.lt.trans half_lt_self mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono ENNReal.instIsOrderedRing ENNReal.coe_le_coe Finset.le_sup_of_le le_self_add NNReal.instCanonicallyOrderedAdd zero_le ENNReal.instCanonicallyOrderedAdd edist_triangle_left add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Metric.mem_ball_self add_le_add_right mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid edist_dist add_le_add ENNReal.ofReal_le_ofReal le_of_not_gt 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.atom_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.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_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Metric.mem_ball Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_nonpos_of_le dist_triangle_left Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.isNat_add mul_le_mul_left covariant_swap_mul_of_covariant_mul ENNReal.coe_le_coe_of_le le_refl Finset.le_sup

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_of_locally_lipschitz 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Dist.dist PseudoMetricSpace.toDist Real.instMul	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	tendsto_iff_dist_tendsto_zero squeeze_zero' Filter.Eventually.of_forall dist_nonneg Filter.mem_of_superset Metric.ball_mem_nhds Continuous.tendsto' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing Real.instIsStrictOrderedRing instOrderTopologyReal continuous_const Continuous.dist continuous_id' dist_self MulZeroClass.mul_zero

---

← Back to Index