lp ∞ A as a C⋆-algebra #
We place these here because, for reasons related to the import hierarchy, they should not be placed in earlier files.
def
instNonUnitalCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal
{I : Type u_1}
{A : I → Type u_2}
[(i : I) → NonUnitalCStarAlgebra (A i)]
:
NonUnitalCStarAlgebra (Subtype fun (x : PreLp A) => Membership.mem (lp A Top.top) x)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal
{I : Type u_1}
{A : I → Type u_2}
[(i : I) → NonUnitalCommCStarAlgebra (A i)]
:
NonUnitalCommCStarAlgebra (Subtype fun (x : PreLp A) => Membership.mem (lp A Top.top) x)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
instNormedRingSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial
{I : Type u_1}
{A : I → Type u_2}
[∀ (i : I), Nontrivial (A i)]
[(i : I) → CStarAlgebra (A i)]
:
NormedRing (Subtype fun (x : PreLp A) => Membership.mem (lp A Top.top) x)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial
{I : Type u_1}
{A : I → Type u_2}
[∀ (i : I), Nontrivial (A i)]
[(i : I) → CommCStarAlgebra (A i)]
:
CommCStarAlgebra (Subtype fun (x : PreLp A) => Membership.mem (lp A Top.top) x)
Equations
- One or more equations did not get rendered due to their size.