α : 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_inf_sub_inf_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 [inf_idem, sub_zero] using h