eventually_isUnit_resolvent — Mathlib

English

The resolvent resolvent a = O cobounded Inv.inv; i.e., resolvent decays like inv along the cobounded filter.

Русский

Резольвентный поток a есть O cobounded Inv.inv; резольвент ведёт себя как обратная единице вдоль cobounded.

LaTeX

$$resolvent a =O[cobounded 𝕜] Inv.inv$$

Lean4

theorem eventually_isUnit_resolvent (a : A) : ∀ᶠ z in cobounded 𝕜, IsUnit (resolvent a z) :=
  by
  rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]
  exact ⟨‖a‖ * ‖(1 : A)‖, trivial, fun _ ↦ isUnit_resolvent.mp ∘ mem_resolventSet_of_norm_lt_mul⟩

Похожие утверждения