English
If the norm of a is small relative to k, precisely if ‖a‖·‖1‖ < ‖k‖, then k lies in the resolvent set of a.
Русский
Если нормa элемента a достаточно мала по отношению к m, точнее if ‖a‖·‖1‖ < ‖k‖, то k принадлежит резольвентному множеству a.
LaTeX
$$$\\text{If } \\|a\\|\\,\\|1\\| < \\|k\\|, \\text{ then } k \\in \\rho(a).$$$
Lean4
theorem mem_resolventSet_of_norm_lt_mul {a : A} {k : 𝕜} (h : ‖a‖ * ‖(1 : A)‖ < ‖k‖) : k ∈ ρ a :=
by
rw [resolventSet, Set.mem_setOf_eq, Algebra.algebraMap_eq_smul_one]
nontriviality A
have hk : k ≠ 0 := ne_zero_of_norm_ne_zero ((mul_nonneg (norm_nonneg _) (norm_nonneg _)).trans_lt h).ne'
letI ku := Units.map ↑ₐ.toMonoidHom (Units.mk0 k hk)
rw [← inv_inv ‖(1 : A)‖, mul_inv_lt_iff₀' (inv_pos.2 <| norm_pos_iff.2 (one_ne_zero : (1 : A) ≠ 0))] at h
have hku : ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹ := by simpa [ku, norm_algebraMap] using h
simpa [ku, sub_eq_add_neg, Algebra.algebraMap_eq_smul_one] using (ku.add (-a) hku).isUnit
