Theorems · Theorem · functional analysis
PiLp.ext
∀ {p : ENNReal} {ι : Type u_1} {α : ι → Type u_2} {x y : PiLp p α}, (∀ (i : ι), x.ofLp i = y.ofLp i) → x = y- Defined in
- Mathlib.Analysis.Normed.Lp.PiLp
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- WithLp.ofLpstatement and proof · cited by 323
- PiLpstatement and proof · cited by 150
- WithLp.ofLp_injectiveproof · cited by 3
Cited by14
Results whose statement or proof uses this declaration.
- contMDiffOn_projIccproof · cited by 4
- LinearIsometryEquiv.piLpCongrLeft_singleproof · cited by 2
- LinearIsometryEquiv.piLpCongrLeft_symmproof · cited by 2
- Matrix.toLpLin_mulproof · cited by 2
- OrthonormalBasis.equiv_apply_basisproof · cited by 2
- LinearMap.posSemidef_toMatrix_iffproof · cited by 1
- Behrend.threeAPFree_sphereproof · cited by 1
- Matrix.toLpLin_oneproof · cited by 1
- Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitaryproof · cited by 1
- Pi.orthonormalBasis_applyproof · cited by 0
- LinearIsometryEquiv.piLpCongrRight_singleproof · cited by 0
- PiLp.ext_iffproof · cited by 0