case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
f : α → β
x✝ y✝ : α
r K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑(Real.toNNReal K)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
f : α → β
x✝ y✝ : α
r K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K * dist x y ≤ ↑(Real.toNNReal K) * dist x y
gcongr
no goals
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
f : α → β
x✝ y✝ : α
r K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑(Real.toNNReal K)
apply Real.le_coe_toNNReal