case h
α : Type u_1
β : Type u_2
γ : Type ?u.15366
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
α : Type u_1
β : Type u_2
γ : Type ?u.15366
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
gcongr
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.15366
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
exact dist_le_diam_of_mem hs hx hy