α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖abs (a - c)‖ + ‖abs (b - d)‖
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ d) ≤ abs (abs (a - c) + abs (b - d))
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖abs (a - c)‖ + ‖abs (b - d)‖
refine' le_trans (solid _) (norm_add_le (|a - c|) (|b - d|))
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ d) ≤ abs (a - c) + abs (b - d)
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ d) ≤ abs (abs (a - c) + abs (b - d))
rw [abs_of_nonneg (|a - c| + |b - d|) (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
no goals
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ d) = abs (a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d))
rw [sub_add_sub_cancel]
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ b) ≤ abs (a - c)

case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (c ⊔ b - c ⊔ d) ≤ abs (b - d)
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ b) + abs (c ⊔ b - c ⊔ d) ≤ abs (a - c) + abs (b - d)
apply add_le_add
no goals
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (a ⊔ b - c ⊔ b) ≤ abs (a - c)
exact abs_sup_sub_sup_le_abs _ _ _
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (b ⊔ c - d ⊔ c) ≤ abs (b - d)
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (c ⊔ b - c ⊔ d) ≤ abs (b - d)
rw [@sup_comm _ _ c, @sup_comm _ _ c]
no goals
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ abs (b ⊔ c - d ⊔ c) ≤ abs (b - d)
exact abs_sup_sub_sup_le_abs _ _ _