English
For a,b,c,d in α, the inequality ‖a ⊓ b − c ⊓ d‖ ≤ ‖a − c‖ + ‖b − d‖ holds.
Русский
Для элементов a,b,c,d из α выполняется неравенство ‖a ⊓ b − c ⊓ d‖ ≤ ‖a − c‖ + ‖b − d‖.
LaTeX
$$$\|a \sqcap b - c \sqcap d\| \le \|a - c\| + \|b - d\|$$$
Lean4
theorem norm_inf_sub_inf_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_inf_sub_inf_le_abs _ _ _
· rw [inf_comm c, inf_comm c]
exact abs_inf_sub_inf_le_abs _ _ _
