English
The map addEquiv 𝕜 A is Lipschitz with constant 2.
Русский
Отображение addEquiv 𝕜 A удовлетворяет липшицевости с константой 2.
LaTeX
$$$$\\text{LipschitzWith}(2,\\ addEquiv\\ 𝕜 A).$$$$
Lean4
theorem lipschitzWith_addEquiv : LipschitzWith 2 (Unitization.addEquiv 𝕜 A) :=
by
rw [← Real.toNNReal_ofNat]
refine AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 fun x => ?_
rw [norm_eq_sup, Prod.norm_def]
refine max_le ?_ ?_
· rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
· nontriviality A
rw [two_mul]
calc
‖x.snd‖ = ‖mul 𝕜 A x.snd‖ := .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
_ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
_ ≤ _ := add_le_add le_sup_right le_sup_left
