rpow_neg_one_eq_cfc_inv — Mathlib

English

The square root equals the functional calculus application of NNReal.sqrt.

Русский

Квадратный корень равен применению функционального расчёта NNReal.sqrt.

LaTeX

$$sqrt a = cfc NNReal.sqrt a$$

Lean4

theorem rpow_neg_one_eq_cfc_inv {A : Type*} [PartialOrder A] [NormedRing A] [StarRing A] [StarOrderedRing A]
    [NormedAlgebra ℝ A] [NonnegSpectrumClass ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) :
    a ^ (-1 : ℝ) = cfc (·⁻¹ : ℝ≥0 → ℝ≥0) a :=
  cfc_congr fun x _ ↦ NNReal.rpow_neg_one x

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