[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
[PROOFSTEP]
simp only [AntilipschitzWith, edist_nndist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
[PROOFSTEP]
simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ K⁻¹ * nndist x y ≤ nndist (f x) (f y)
[PROOFSTEP]
simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ ↑K⁻¹ * dist x y ≤ dist (f x) (f y)
[PROOFSTEP]
exact_mod_cast hf.mul_le_nndist x y
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α✝ → β✝
α : Type u_4
β : Type u_5
inst✝¹ : EMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y
[PROOFSTEP]
simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)
[PROOFSTEP]
exact ENNReal.div_le_of_le_mul' (hf x y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
⊢ edist x y ≤ ↑1 * edist (id x) (id y)
[PROOFSTEP]
simp only [ENNReal.coe_one, one_mul, id, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑(Kf * Kg) * edist ((g ∘ f) x) ((g ∘ f) y)
[PROOFSTEP]
rw [ENNReal.coe_mul, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
s : Set α
hf : AntilipschitzWith K (Set.restrict s f)
g : β → α
t : Set β
g_maps : MapsTo g t s
g_inv : RightInvOn g f t
x y : ↑t
⊢ edist (Set.restrict t g x) (Set.restrict t g y) ≤ ↑K * edist x y
[PROOFSTEP]
simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_eq, Subtype.coe_mk] using
  hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
⊢ LipschitzWith K g
[PROOFSTEP]
intro x y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) ≤ ↑K * edist x y
[PROOFSTEP]
have := hf (g x) (g y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ ↑K * edist (f (g x)) (f (g y))
⊢ edist (g x) (g y) ≤ ↑K * edist x y
[PROOFSTEP]
rwa [hg x, hg y] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} ⊆ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ Prod.map f f ⁻¹' {p | edist p.fst p.snd < (↑K)⁻¹ * ε} ⊆ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
refine' fun x hx => (hf x.1 x.2).trans_lt _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < (↑K)⁻¹ * ε}
⊢ ↑K * edist (f x.fst) (f x.snd) < ε
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < ε / ↑K}
⊢ ↑K * edist (f x.fst) (f x.snd) < ε
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < ε / ↑K}
⊢ edist (f x.fst) (f x.snd) * ↑K < ε
[PROOFSTEP]
exact ENNReal.mul_lt_of_lt_div hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f : α → β
inst✝ : Subsingleton α
K : ℝ≥0
x y : α
⊢ edist x y ≤ ↑K * edist (f x) (f y)
[PROOFSTEP]
simp only [Subsingleton.elim x y, edist_self, zero_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
hs : Metric.Bounded s
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ ↑K * dist (f x) (f y) ≤ ↑K * diam s
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
hs : Metric.Bounded s
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ dist (f x) (f y) ≤ diam s
[PROOFSTEP]
exact dist_le_diam_of_mem hs hx hy
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
⊢ ProperSpace β
[PROOFSTEP]
refine ⟨fun x₀ r => ?_⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
let K := f ⁻¹' closedBall x₀ r
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
have A : IsClosed K := isClosed_ball.preimage f_cont
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
have B : Bounded K := hK.bounded_preimage bounded_closedBall
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
convert this.image f_cont
[GOAL]
case h.e'_3
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K
[PROOFSTEP]
exact (hf.image_preimage _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist x y ≤ ↑K * edist (g x) (g y)
[PROOFSTEP]
simpa only [hg _] using hf (g x) (g y)
