α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y
rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
no goals
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
exact norm_sup_sub_sup_le_norm x y z