English
If 𝕜 is a normed field and R is a normed algebra over 𝕜, then C(α,R)₀ is a NormedSpace over 𝕜; the scalar action is compatible with the norm: ‖r f‖ ≤ ‖r‖ ‖f‖.
Русский
Если 𝕜 — нормированное поле и R — нормированная алгебра над 𝕜, то C(α,R)₀ является нормированным пространством над 𝕜; действие скаляра совместимо с нормой.
LaTeX
$$$\\|r\\cdot f\\| \\le \\|r\\| \\|f\\|$$$
Lean4
noncomputable instance (priority := 100) instContinuousSqrtRCLike {𝕜 : Type*} [RCLike 𝕜] : ContinuousSqrt 𝕜
where
sqrt := ((↑) ∘ (√·) ∘ re ∘ (fun z ↦ z.2 - z.1))
continuousOn_sqrt := by fun_prop
sqrt_nonneg _ _ := by simp
sqrt_mul_sqrt x
hx := by
simp only [Function.comp_apply, ]
rw [← sub_nonneg] at hx
obtain hx' := nonneg_iff.mp hx |>.right
rw [← conj_eq_iff_im, conj_eq_iff_re] at hx'
rw [← ofReal_mul, Real.mul_self_sqrt, hx', add_sub_cancel]
simpa using nonneg_iff.mp hx |>.left
