norm_cfcₙ_one_sub_one_add_inv_lt_one

English

The norm of the cfcₙ functional calculus of a nonunital C*-algebra element with the 1 - (1+x)^{-1} shape is strictly less than 1.

Русский

Нормa функционала cfcₙ для элемента без единицы в C*-алгебре с формой 1 - (1+x)^{-1} строго меньше единицы.

LaTeX

$$$$ \| cfc_\n\left( f(x) = 1 - (1+x)^{-1} \right)(a) \| < 1 $$$$

Lean4

theorem norm_cfcₙ_one_sub_one_add_inv_lt_one (a : A) : ‖cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) a‖ < 1 :=
  nnnorm_cfcₙ_nnreal_lt fun x _ ↦
    tsub_lt_self zero_lt_one
      (by positivity)
        -- the calls to `fun_prop` with a discharger set off the linter

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