Theorems · Theorem · functional analysis
norm_cfc_lt_iff
∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
[inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
(a : A) {c : ℝ},
0 < c →
autoParam (ContinuousOn f (spectrum 𝕜 a)) norm_cfc_lt_iff._auto_1 →
autoParam (p a) norm_cfc_lt_iff._auto_3 → (‖cfc f a‖ < c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖ < c)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- RCLikestatement and proof · cited by 2,829
- StarRingstatement and proof · cited by 1,686
- ContinuousOnstatement and proof · cited by 1,411
- NormedAlgebrastatement and proof · cited by 1,165
- NormedRingstatement and proof · cited by 924
- LE.le.trans_ltproof · cited by 795
- spectrumstatement and proof · cited by 510
- cfcstatement and proof · cited by 228
- IsometricContinuousFunctionalCalculusstatement and proof · cited by 62
Cited by1
Results whose statement or proof uses this declaration.
- nnnorm_cfc_lt_iffproof · cited by 0