Lipschitz continuous functions #
This file develops Lipschitz continuous functions further with some results that depend on algebra.
theorem
LipschitzWith.cauchySeq_comp
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : LipschitzWith K f)
{u : ℕ → α}
(hu : CauchySeq u)
:
theorem
LipschitzOnWith.cauchySeq_comp
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{s : Set α}
{f : α → β}
(hf : LipschitzOnWith K f s)
{u : ℕ → α}
(hu : CauchySeq u)
(h'u : Set.range u ⊆ s)
:
theorem
continuousAt_of_locally_lipschitz
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{f : α → β}
{x : α}
{r : ℝ}
(hr : 0 < r)
(K : ℝ)
(h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x)
:
ContinuousAt f x
If a function is locally Lipschitz around a point, then it is continuous at this point.