English
Same type of inequality as above with the infimum structure, i.e. ‖a ⊓ b − c ⊓ d‖ ≤ ‖a − c‖ + ‖b − d‖.
Русский
Та же по форме неравность для инфимума: ‖a ⊓ b − c ⊓ d‖ ≤ ‖a − c‖ + ‖b − d‖.
LaTeX
$$$\|a \inf b - c \inf d\| \le \|a - c\| + \|b - d\|$$$
Lean4
theorem norm_sup_sub_sup_le_add_norm (a b c d : α) : ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖ :=
by
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
calc
|a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
_ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := (abs_add_le _ _)
_ ≤ |a - c| + |b - d| := by
gcongr ?_ + ?_
· exact abs_sup_sub_sup_le_abs _ _ _
· rw [sup_comm c, sup_comm c]
exact abs_sup_sub_sup_le_abs _ _ _
