α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
have h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_sup_sub_sup_le_add_norm x y 0 0
no goals
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
simpa only [sup_idem, sub_zero] using h