Skip to content

Commit

Permalink
fix(topology/metric_space/lipschitz): typo (#16962)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Oct 14, 2022
1 parent 34f53b6 commit e623a7e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/topology/metric_space/lipschitz.lean
Expand Up @@ -223,7 +223,7 @@ end
protected lemma prod_mk_left (a : α) : lipschitz_with 1 (prod.mk a : β → α × β) :=
by simpa only [max_eq_right zero_le_one] using (lipschitz_with.const a).prod lipschitz_with.id

protected lemma prod_mk_right (b : α) : lipschitz_with 1 (λ a : α, (a, b)) :=
protected lemma prod_mk_right (b : β) : lipschitz_with 1 (λ a : α, (a, b)) :=
by simpa only [max_eq_left zero_le_one] using lipschitz_with.id.prod (lipschitz_with.const b)

protected lemma uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, lipschitz_with Kα (λ a, f a b))
Expand Down

0 comments on commit e623a7e

Please sign in to comment.