α : Type u_1
β : Type u_2
γ : Type ?u.10552
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 < ε}
α : Type u_1
β : Type u_2
γ : Type ?u.10552
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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 < ε}
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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 < ε}
refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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) < ε
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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 < ε}
refine' fun x hx => (hf x.1 x.2).trans_lt _
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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) < ε
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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) < ε
rw [mul_comm, ← div_eq_mul_inv] at hx
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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 < ε
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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) < ε
rw [mul_comm]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.10552
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 < ε
exact ENNReal.mul_lt_of_lt_div hx