Loogle!

Result

Found 140 declarations mentioning LipschitzOnWith.

• LipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) (s : Set α) : Prop
• lipschitzOnWith_empty 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) : LipschitzOnWith K f ∅
• lipschitzOnWith_univ 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} : LipschitzOnWith K f Set.univ ↔ LipschitzWith K f
• LipschitzWith.lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} (h : LipschitzWith K f) : LipschitzOnWith K f s
• LipschitzOnWith.uniformContinuousOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) : UniformContinuousOn f s
• LipschitzOnWith.continuousOn 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) : ContinuousOn f s
• LipschitzOnWith.mono 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s t : Set α} {f : α → β} (hf : LipschitzOnWith K f t) (h : s ⊆ t) : LipschitzOnWith K f s
• LipschitzOnWith.weaken 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {K' : NNReal} (h : K ≤ K') : LipschitzOnWith K' f s
• LipschitzOnWith.to_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s → LipschitzWith K (s.domRestrict f)
• lipschitzOnWith_iff_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s ↔ LipschitzWith K (s.domRestrict f)
• LipschitzOnWith.zero_iff 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} [PseudoEMetricSpace α] {s : Set α} {β : Type u_1} [EMetricSpace β] (f : α → β) : LipschitzOnWith 0 f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y
• LipschitzWith.comp_lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf Kg : NNReal} {f : β → γ} {g : α → β} {s : Set α} (hf : LipschitzWith Kf f) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf * Kg) (f ∘ g) s
• LipschitzOnWith.prodMk 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {s : Set α} {f : α → β} {g : α → γ} {Kf Kg : NNReal} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s
• LipschitzOnWith.comp 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {K : NNReal} {s : Set α} {f : α → β} {g : β → γ} {t : Set β} {Kg : NNReal} (hg : LipschitzOnWith Kg g t) (hf : LipschitzOnWith K f s) (hmaps : Set.MapsTo f s t) : LipschitzOnWith (Kg * K) (g ∘ f) s
• LipschitzOnWith.mapsToRestrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {t : Set β} (h : Set.MapsTo f s t) : LipschitzOnWith K f s → LipschitzWith K (Set.MapsTo.restrict f s t h)
• Set.MapsTo.lipschitzOnWith_iff_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {t : Set β} (h : Set.MapsTo f s t) : LipschitzOnWith K f s ↔ LipschitzWith K (Set.MapsTo.restrict f s t h)
• lipschitzOnWith_restrict 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {t : Set ↑s} : LipschitzOnWith K (s.domRestrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)
• LipschitzOnWith.edist_le_mul_of_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {r : ENNReal} (hr : edist x y ≤ r) : edist (f x) (f y) ≤ ↑K * r
• LipschitzOnWith.edist_lt_of_edist_lt_div 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {d : ENNReal} (hd : edist x y < d / ↑K) : edist (f x) (f y) < d
• continuousOn_prod_of_continuousOn_lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal) (ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• continuousOn_prod_of_continuousOn_lipschitzOnWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal) (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) (hb : ∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β} (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : NNReal) (ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β} (ht' : t' ⊆ t) (htt' : t ⊆ closure t') (K : NNReal) (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) (hb : ∀ b ∈ t', ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)
• LipschitzOnWith.ediam_image2_le 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} (s : Set α) (t : Set β) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Metric.ediam (Set.image2 f s t) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
• isClosed_setOfPred_lipschitzOnWith 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (s : Set α) : IsClosed {f | LipschitzOnWith K f s}
• isClosed_setOf_lipschitzOnWith 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (s : Set α) : IsClosed {f | LipschitzOnWith K f s}
• LipschitzOnWith.closure 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} {K : NNReal} (hcont : ContinuousOn f (closure s)) (hf : LipschitzOnWith K f s) : LipschitzOnWith K f (closure s)
• lipschitzOnWith_closure_iff 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} {K : NNReal} (hcont : ContinuousOn f (closure s)) : LipschitzOnWith K f (closure s) ↔ LipschitzOnWith K f s
• LipschitzOnWith.extend_real 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} [PseudoMetricSpace α] {f : α → ℝ} {s : Set α} {K : NNReal} (hf : LipschitzOnWith K f s) : ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
• LipschitzOnWith.mk_one 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {f : α → β} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) : LipschitzOnWith 1 f s
• LipschitzOnWith.of_le_add 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) : LipschitzOnWith 1 f s
• LipschitzOnWith.extend_pi 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {ι : Type x} [PseudoMetricSpace α] [Fintype ι] {f : α → ι → ℝ} {s : Set α} {K : NNReal} (hf : LipschitzOnWith K f s) : ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
• LipschitzOnWith.dist_le_mul 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s → ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
• LipschitzOnWith.of_dist_le' 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {f : α → β} {K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) : LipschitzOnWith K.toNNReal f s
• LipschitzOnWith.of_dist_le_mul 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y) → LipschitzOnWith K f s
• lipschitzOnWith_iff_dist_le_mul 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
• LipschitzOnWith.le_add_mul 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} {K : NNReal} (h : LipschitzOnWith K f s) {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) : f x ≤ f y + ↑K * dist x y
• LipschitzOnWith.of_le_add_mul 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : NNReal) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y) : LipschitzOnWith K f s
• LipschitzOnWith.of_le_add_mul' 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : ℝ) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith K.toNNReal f s
• LipschitzOnWith.iff_le_add_mul 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} {K : NNReal} : LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y
• LipschitzOnWith.isBounded_image2 📋 Mathlib.Topology.MetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} {s : Set α} {t : Set β} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t)
• LipschitzOnWith.inv 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f s → LipschitzOnWith K f⁻¹ s
• LipschitzOnWith.neg 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f s → LipschitzOnWith K (-f) s
• LipschitzOnWith.of_inv 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f⁻¹ s → LipschitzOnWith K f s
• LipschitzOnWith.of_neg 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K (-f) s → LipschitzOnWith K f s
• lipschitzOnWith_inv_iff 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s
• lipschitzOnWith_neg_iff 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} : LipschitzOnWith K (-f) s ↔ LipschitzOnWith K f s
• LipschitzOnWith.div 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun x => f x / g x) s
• LipschitzOnWith.sub 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun x => f x - g x) s
• LipschitzOnWith.add 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun x => f x + g x) s
• LipschitzOnWith.mul 📋 Mathlib.Analysis.Normed.Group.Uniform
  {α : Type u_4} {E : Type u_5} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf Kg : NNReal} {f g : α → E} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf + Kg) (fun x => f x * g x) s
• LipschitzOnWith.norm_div_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedCommGroup E] [SeminormedCommGroup F] {f : E → F} {C : NNReal} {s : Set E} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
• LipschitzOnWith.norm_sub_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {C : NNReal} {s : Set E} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
• lipschitzOnWith_iff_norm_div_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedCommGroup E] [SeminormedCommGroup F] {f : E → F} {C : NNReal} {s : Set E} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
• lipschitzOnWith_iff_norm_sub_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {C : NNReal} {s : Set E} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
• LipschitzOnWith.norm_div_le_of_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedCommGroup E] [SeminormedCommGroup F] {f : E → F} {C : NNReal} {s : Set E} {a b : E} {r : ℝ} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ ↑C * r
• LipschitzOnWith.norm_sub_le_of_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {C : NNReal} {s : Set E} {a b : E} {r : ℝ} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a - b‖ ≤ r) : ‖f a - f b‖ ≤ ↑C * r
• LipschitzOnWith.norm_inv_mul_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
• LipschitzOnWith.norm_neg_add_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖-f x + f y‖ ≤ ↑C * ‖-x + y‖
• lipschitzOnWith_iff_norm_inv_mul_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
• lipschitzOnWith_iff_norm_neg_add_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖-f x + f y‖ ≤ ↑C * ‖-x + y‖
• LipschitzOnWith.norm_inv_mul_le_of_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a⁻¹ * b‖ ≤ r) : ‖(f a)⁻¹ * f b‖ ≤ ↑C * r
• LipschitzOnWith.norm_neg_add_le_of_le 📋 Mathlib.Analysis.Normed.Group.Uniform
  {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {a b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖-a + b‖ ≤ r) : ‖-f a + f b‖ ≤ ↑C * r
• LocallyLipschitzOn.exists_lipschitzOnWith_of_compact 📋 Mathlib.Topology.Algebra.MetricSpace.Lipschitz
  {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} (hs : IsCompact s) (hf : LocallyLipschitzOn s f) : ∃ K, LipschitzOnWith K f s
• LipschitzOnWith.cauchySeq_comp 📋 Mathlib.Topology.Algebra.MetricSpace.Lipschitz
  {α : 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) : CauchySeq (f ∘ u)
• LipschitzOnWith.extend_finite_dimension 📋 Mathlib.Analysis.Normed.Module.FiniteDimension
  {α : Type u_1} [PseudoMetricSpace α] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set α} {f : α → E'} {K : NNReal} (hf : LipschitzOnWith K f s) : ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ Set.EqOn f g s
• HasStrictFDerivAt.exists_lipschitzOnWith 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} (hf : HasStrictFDerivAt f f' x) : ∃ K, ∃ s ∈ nhds x, LipschitzOnWith K f s
• norm_fderiv_le_of_lipschitzOn 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖fderiv 𝕜 f x₀‖ ≤ ↑C
• HasFDerivAt.le_of_lipschitzOn 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {s : Set E} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ ↑C
• HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} (hf : HasStrictFDerivAt f f' x) (K : NNReal) (hK : ‖f'‖₊ < K) : ∃ s ∈ nhds x, LipschitzOnWith K f s
• norm_deriv_le_of_lipschitzOn 📋 Mathlib.Analysis.Calculus.Deriv.Basic
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖deriv f x₀‖ ≤ ↑C
• HasDerivAt.le_of_lipschitzOn 📋 Mathlib.Analysis.Calculus.Deriv.Basic
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀) {s : Set 𝕜} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ ↑C
• Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f f' : 𝕜 → G} {s : Set 𝕜} {C : NNReal} (hs : Convex ℝ s) (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C) : LipschitzOnWith C f s
• Convex.lipschitzOnWith_of_nnnorm_derivWithin_le 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} {C : NNReal} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) (bound : ∀ x ∈ s, ‖derivWithin f s x‖₊ ≤ C) : LipschitzOnWith C f s
• Convex.lipschitzOnWith_of_nnnorm_deriv_le 📋 Mathlib.Analysis.Calculus.MeanValue
  {𝕜 : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : 𝕜 → G} {s : Set 𝕜} {C : NNReal} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ x ∈ s, ‖deriv f x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s
• Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G} (hs : Convex ℝ s) {f : E → G} (hder : ∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) (hcont : ContinuousWithinAt f' s x) : ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
• Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal} (hf : DifferentiableOn 𝕜 f s) (bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s
• Convex.lipschitzOnWith_of_nnnorm_fderiv_le 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ x ∈ s, ‖fderiv 𝕜 f x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s
• Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {C : NNReal} (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s
• Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt 📋 Mathlib.Analysis.Calculus.MeanValue
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G} (hs : Convex ℝ s) {f : E → G} (hder : ∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) (hcont : ContinuousWithinAt f' s x) (K : NNReal) (hK : ‖f' x‖₊ < K) : ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
• hasDerivAt_integral_of_dominated_loc_of_lip 📋 Mathlib.Analysis.Calculus.ParametricIntegral
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {bound : α → ℝ} {F : 𝕜 → α → E} {x₀ : 𝕜} {s : Set 𝕜} {F' : α → E} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) s) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' a) x₀) : MeasureTheory.Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
• hasFDerivAt_integral_of_dominated_loc_of_lip_interval 📋 Mathlib.Analysis.Calculus.ParametricIntegral
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {s : Set H} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), HasFDerivAt (fun x => F x t) (F' t) x₀) : IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
• hasFDerivAt_integral_of_dominated_loc_of_lip 📋 Mathlib.Analysis.Calculus.ParametricIntegral
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H} {F' : α → H →L[𝕜] E} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) s) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) : MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
• intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip 📋 Mathlib.Analysis.Calculus.ParametricIntervalIntegral
  {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lipsch : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasDerivAt (fun x => F x t) (F' t) x₀) : IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
• intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip 📋 Mathlib.Analysis.Calculus.ParametricIntervalIntegral
  {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasFDerivAt (fun x => F x t) (F' t) x₀) : IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
• ContDiffAt.exists_lipschitzOnWith 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {𝕂 : Type u_1} [RCLike 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) : ∃ K, ∃ t ∈ nhds x, LipschitzOnWith K f t
• ContDiffOn.exists_lipschitzOnWith 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (hn : n ≠ 0) (hs : Convex ℝ s) (hs' : IsCompact s) : ∃ K, LipschitzOnWith K f s
• ContDiffWithinAt.exists_lipschitzOnWith 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} (hf : ContDiffWithinAt ℝ 1 f s x) (hs : Convex ℝ s) : ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
• ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {𝕂 : Type u_1} [RCLike 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) (K : NNReal) (hK : ‖fderiv 𝕂 f x‖₊ < K) : ∃ t ∈ nhds x, LipschitzOnWith K f t
• HasFTaylorSeriesUpToOn.exists_lipschitzOnWith 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E} (hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) : ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
• HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E} (hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) (K : NNReal) (hK : ‖p x 1‖₊ < K) : ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
• ApproximatesLinearOn.lipschitzOnWith 📋 Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} : ApproximatesLinearOn f f' s c → LipschitzOnWith c (f - ⇑f') s
• LipschitzOnWith.approximatesLinearOn 📋 Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} : LipschitzOnWith c (f - ⇑f') s → ApproximatesLinearOn f f' s c
• ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith 📋 Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} : ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s
• LipschitzOnWith.locallyBoundedVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {M : Type u_3} [PseudoEMetricSpace M] {f : ℝ → M} {C : NNReal} {s : Set ℝ} (hf : LipschitzOnWith C f s) : LocallyBoundedVariationOn f s
• LipschitzOnWith.comp_boundedVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {M : Type u_3} [PseudoEMetricSpace M] {F : Type u_4} [PseudoEMetricSpace F] {f : M → F} {C : NNReal} {t : Set M} (hf : LipschitzOnWith C f t) {g : α → M} {s : Set α} (hg : Set.MapsTo g s t) (h : BoundedVariationOn g s) : BoundedVariationOn (f ∘ g) s
• LipschitzOnWith.comp_locallyBoundedVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {M : Type u_3} [PseudoEMetricSpace M] {F : Type u_4} [PseudoEMetricSpace F] {f : M → F} {C : NNReal} {t : Set M} (hf : LipschitzOnWith C f t) {g : α → M} {s : Set α} (hg : Set.MapsTo g s t) (h : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f ∘ g) s
• LipschitzOnWith.comp_eVariationOn_le 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {M : Type u_3} [PseudoEMetricSpace M] {F : Type u_4} [PseudoEMetricSpace F] {f : M → F} {C : NNReal} {t : Set M} (h : LipschitzOnWith C f t) {g : α → M} {s : Set α} (hg : Set.MapsTo g s t) : eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s
• LipschitzOnWith.ae_differentiableWithinAt_of_mem_real 📋 Mathlib.Analysis.BoundedVariation
  {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal} {f : ℝ → V} {s : Set ℝ} (h : LipschitzOnWith C f s) : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
• LipschitzOnWith.ae_differentiableWithinAt_real 📋 Mathlib.Analysis.BoundedVariation
  {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal} {f : ℝ → V} {s : Set ℝ} (h : LipschitzOnWith C f s) (hs : MeasurableSet s) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
• LipschitzOnWith.uniformEquicontinuousOn 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] (f : α → γ → β) (K : NNReal) {s : Set γ} (h : ∀ (c : α), LipschitzOnWith K (f c) s) : UniformEquicontinuousOn f s
• UniformFun.lipschitzOnWith_iff 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → UniformFun α β} {K : NNReal} {s : Set γ} : LipschitzOnWith K f s ↔ ∀ (c : α), LipschitzOnWith K (fun x => UniformFun.toFun (f x) c) s
• UniformFun.lipschitzOnWith_ofFun_iff 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → α → β} {K : NNReal} {s : Set γ} : LipschitzOnWith K (fun x => UniformFun.ofFun (f x)) s ↔ ∀ (c : α), LipschitzOnWith K (fun x => f x c) s
• UniformOnFun.lipschitzOnWith_iff 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {f : γ → UniformOnFun α β 𝔖} {K : NNReal} {s : Set γ} : LipschitzOnWith K f s ↔ ∀ c ∈ ⋃₀ 𝔖, LipschitzOnWith K (fun x => (UniformOnFun.toFun 𝔖) (f x) c) s
• lipschitzOnWith_cfc_fun_of_subset 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [MetricSpace A] [Algebra R A] [IsometricContinuousFunctionalCalculus R A p] (a : A) {s : Set R} (hs : spectrum R a ⊆ s) : LipschitzOnWith 1 (fun f => cfc ((UniformOnFun.toFun {s}) f) a) {f | ContinuousOn ((UniformOnFun.toFun {s}) f) s}
• lipschitzOnWith_cfc_fun 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [MetricSpace A] [Algebra R A] [IsometricContinuousFunctionalCalculus R A p] (a : A) : LipschitzOnWith 1 (fun f => cfc ((UniformOnFun.toFun {spectrum R a}) f) a) {f | ContinuousOn ((UniformOnFun.toFun {spectrum R a}) f) (spectrum R a)}
• lipschitzOnWith_cfcₙ_fun_of_subset 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) {s : Set R} (hs : quasispectrum R a ⊆ s) : LipschitzOnWith 1 (fun f => cfcₙ ((UniformOnFun.toFun {s}) f) a) {f | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0}
• lipschitzOnWith_cfcₙ_fun 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
  (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) : LipschitzOnWith 1 (fun f => cfcₙ ((UniformOnFun.toFun {quasispectrum R a}) f) a) {f | ContinuousOn ((UniformOnFun.toFun {quasispectrum R a}) f) (quasispectrum R a) ∧ f 0 = 0}
• LipschitzOnWith.coordinate 📋 Mathlib.Analysis.Normed.Lp.lpSpace
  {α : Type u_3} {ι : Type u_5} [PseudoMetricSpace α] (f : α → ↥(lp (fun x => ℝ) ⊤)) (s : Set α) (K : NNReal) : LipschitzOnWith K f s ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
• LipschitzOnWith.holderOnWith 📋 Mathlib.Topology.MetricSpace.Holder
  {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {f : X → Y} {s : Set X} : LipschitzOnWith C f s → HolderOnWith C 1 f s
• holderOnWith_one 📋 Mathlib.Topology.MetricSpace.Holder
  {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {f : X → Y} {s : Set X} : HolderOnWith C 1 f s ↔ LipschitzOnWith C f s
• norm_lineDeriv_le_of_lipschitzOn 📋 Mathlib.Analysis.Calculus.LineDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {v : E} {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖
• HasLineDerivAt.le_of_lipschitzOn 📋 Mathlib.Analysis.Calculus.LineDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {v : E} {f : E → F} {f' : F} {x₀ : E} (hf : HasLineDerivAt 𝕜 f f' x₀ v) {s : Set E} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ ↑C * ‖v‖
• LipschitzOnWith.ae_differentiableWithinAt_of_mem_of_real 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {s : Set E} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzOnWith C f s) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
• LipschitzOnWith.ae_differentiableWithinAt 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : NNReal} {s : Set E} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F} (hf : LipschitzOnWith C f s) (hs : MeasurableSet s) : ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
• LipschitzOnWith.ae_differentiableWithinAt_of_mem 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : NNReal} {s : Set E} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F} (hf : LipschitzOnWith C f s) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
• LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {ι : Type u_3} [Fintype ι] {f : E → ι → ℝ} {s : Set E} (hf : LipschitzOnWith C f s) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
• LipschitzOnWith.absolutelyContinuousOnInterval 📋 Mathlib.MeasureTheory.Function.AbsolutelyContinuous
  {X : Type u_1} [PseudoMetricSpace X] {a b : ℝ} {f : ℝ → X} {K : NNReal} (hfK : LipschitzOnWith K f (Set.uIcc a b)) : AbsolutelyContinuousOnInterval f a b
• LipschitzOnWith.comp_absolutelyContinuousOnInterval 📋 Mathlib.MeasureTheory.Function.AbsolutelyContinuous
  {X : Type u_1} [PseudoMetricSpace X] {Y : Type u_3} [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} {t : Set X} (hf : LipschitzOnWith K f t) {g : ℝ → X} {a b : ℝ} (hg : Set.MapsTo g (Set.uIcc a b) t) (h : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (f ∘ g) a b
• ConcaveOn.exists_lipschitzOnWith_of_isBounded 📋 Mathlib.Analysis.Convex.Continuous
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ} (hf : ConcaveOn ℝ (Metric.ball x₀ r) f) (hr : r' < r) (hf' : Bornology.IsBounded (f '' Metric.ball x₀ r)) : ∃ K, LipschitzOnWith K f (Metric.ball x₀ r')
• ConvexOn.exists_lipschitzOnWith_of_isBounded 📋 Mathlib.Analysis.Convex.Continuous
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ} (hf : ConvexOn ℝ (Metric.ball x₀ r) f) (hr : r' < r) (hf' : Bornology.IsBounded (f '' Metric.ball x₀ r)) : ∃ K, LipschitzOnWith K f (Metric.ball x₀ r')
• ConcaveOn.lipschitzOnWith_of_abs_le 📋 Mathlib.Analysis.Convex.Continuous
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ} (hf : ConcaveOn ℝ (Metric.ball x₀ r) f) (hε : 0 < ε) (hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M) : LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))
• ConvexOn.lipschitzOnWith_of_abs_le 📋 Mathlib.Analysis.Convex.Continuous
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ} (hf : ConvexOn ℝ (Metric.ball x₀ r) f) (hε : 0 < ε) (hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M) : LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))
• LipschitzOnWith.hausdorffMeasure_image_le 📋 Mathlib.MeasureTheory.Measure.Hausdorff
  {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {K : NNReal} {f : X → Y} {s : Set X} (h : LipschitzOnWith K f s) {d : ℝ} (hd : 0 ≤ d) : (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s
• LipschitzOnWith.dimH_image_le 📋 Mathlib.Topology.MetricSpace.HausdorffDimension
  {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] {K : NNReal} {f : X → Y} {s : Set X} (h : LipschitzOnWith K f s) : dimH (f '' s) ≤ dimH s
• dimH_range_le_of_locally_lipschitzOn 📋 Mathlib.Topology.MetricSpace.HausdorffDimension
  {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [SecondCountableTopology X] {f : X → Y} (hf : ∀ (x : X), ∃ C, ∃ s ∈ nhds x, LipschitzOnWith C f s) : dimH (Set.range f) ≤ dimH Set.univ
• dimH_image_le_of_locally_lipschitzOn 📋 Mathlib.Topology.MetricSpace.HausdorffDimension
  {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [SecondCountableTopology X] {f : X → Y} {s : Set X} (hf : ∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, LipschitzOnWith C f t) : dimH (f '' s) ≤ dimH s
• dist_le_of_trajectories_ODE_of_mem 📋 Mathlib.Analysis.ODE.Gronwall
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b δ : ℝ} (hv : ∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : dist (f a) (g a) ≤ δ) (t : ℝ) : t ∈ Set.Icc a b → dist (f t) (g t) ≤ δ * Real.exp (↑K * (t - a))
• dist_le_of_approx_trajectories_ODE_of_mem 📋 Mathlib.Analysis.ODE.Gronwall
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g f' g' : ℝ → E} {a b εf εg δ : ℝ} (hv : ∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t) (f_bound : ∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t) (g_bound : ∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : dist (f a) (g a) ≤ δ) (t : ℝ) : t ∈ Set.Icc a b → dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
• IsPicardLindelof.lipschitzOnWith 📋 Mathlib.Analysis.ODE.PicardLindelof
  {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (self : IsPicardLindelof f t₀ x₀ a r L K) (t : ℝ) : t ∈ Set.Icc tmin tmax → LipschitzOnWith K (f t) (Metric.closedBall x₀ ↑a)
• IsPicardLindelof.of_time_independent 📋 Mathlib.Analysis.ODE.PicardLindelof
  {E : Type u_1} [NormedAddCommGroup E] {f : E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hb : ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f x‖ ≤ ↑L) (hl : LipschitzOnWith K f (Metric.closedBall x₀ ↑a)) (hm : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r) : IsPicardLindelof (fun x => f) t₀ x₀ a r L K
• IsPicardLindelof.mk 📋 Mathlib.Analysis.ODE.PicardLindelof
  {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (lipschitzOnWith : ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith K (f t) (Metric.closedBall x₀ ↑a)) (continuousOn : ∀ x ∈ Metric.closedBall x₀ ↑a, ContinuousOn (fun x_1 => f x_1 x) (Set.Icc tmin tmax)) (norm_le : ∀ t ∈ Set.Icc tmin tmax, ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f t x‖ ≤ ↑L) (mul_max_le : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r) : IsPicardLindelof f t₀ x₀ a r L K
• ODE_solution_unique_univ 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {t₀ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : f = g
• IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ α, (∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧ ∃ L', ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith L' (fun x => α x t) (Metric.closedBall x₀ ↑r)
• ODE_solution_unique_of_eventually 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {t₀ : ℝ} (hv : ∀ᶠ (t : ℝ) in nhds t₀, LipschitzOnWith K (v t) (s t)) (hf : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : f =ᶠ[nhds t₀] g
• ODE_solution_unique_of_mem_Ioo 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b t₀ : ℝ} (hv : ∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Set.Ioo a b) (hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : Set.EqOn f g (Set.Ioo a b)
• ODE_solution_unique_of_mem_Icc_left 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b : ℝ} (hv : ∀ t ∈ Set.Ioc a b, LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt f (v t (f t)) (Set.Iic t) t) (hfs : ∀ t ∈ Set.Ioc a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt g (v t (g t)) (Set.Iic t) t) (hgs : ∀ t ∈ Set.Ioc a b, g t ∈ s t) (hb : f b = g b) : Set.EqOn f g (Set.Icc a b)
• ODE_solution_unique_of_mem_Icc_right 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b : ℝ} (hv : ∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : f a = g a) : Set.EqOn f g (Set.Icc a b)
• ODE_solution_unique_of_mem_Icc 📋 Mathlib.Analysis.ODE.ExistUnique
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b t₀ : ℝ} (hv : ∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Set.Ioo a b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t) (hfs : ∀ t ∈ Set.Ioo a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t) (hgs : ∀ t ∈ Set.Ioo a b, g t ∈ s t) (heq : f t₀ = g t₀) : Set.EqOn f g (Set.Icc a b)
• LipschitzOnWith.extend_lp_infty 📋 Mathlib.Topology.MetricSpace.Kuratowski
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {ι : Type u_1} {f : α → ↥(lp (fun x => ℝ) ⊤)} {K : NNReal} (hfl : LipschitzOnWith K f s) : ∃ g, LipschitzWith K g ∧ Set.EqOn f g s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59