Theorems · Theorem · functional analysis
ContinuousLinearMap.isBoundedLinearMap
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(f : E →L[𝕜] F), IsBoundedLinearMap 𝕜 ⇑fA continuous linear map satisfies IsBoundedLinearMap
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHom.idstatement and proof · cited by 18,349
- NormedSpacestatement and proof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- ContinuousLinearMapstatement and proof · cited by 5,352
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- ContinuousLinearMap.toLinearMapproof · cited by 528
- IsLinearMapproof · cited by 41
- IsBoundedLinearMapstatement · cited by 39
- LinearMap.isLinearproof · cited by 10
- ContinuousLinearMap.boundproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.contDiffproof · cited by 18
- spectralNorm_uniqueproof · cited by 3
- isBoundedLinearMap_continuousMultilinearMap_comp_linearproof · cited by 1
- isBoundedLinearMap_prod_multilinearproof · cited by 0
- IsBoundedBilinearMap.isBoundedLinearMap_derivproof · cited by 0
- IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMapproof · cited by 0