instance
PiLp.addCommGroup
{ι : Type u_1}
{β : ι → Type u_2}
{p : ENNReal}
[(i : ι) → AddCommGroup (β i)]
:
AddCommGroup (PiLp p β)
Equations
- PiLp.addCommGroup = let __src := Pi.addCommGroup; AddCommGroup.mk ⋯
@[simp]
theorem
PiLp.equiv_zero'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
:
(WithLp.equiv p ((i : ι) → β i)) 0 = 0
@[simp]
theorem
PiLp.equiv_symm_zero'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
:
(WithLp.equiv p ((i : ι) → β i)).symm 0 = 0
@[simp]
theorem
PiLp.equiv_add'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
{x : (i : ι) → β i}
{y : (i : ι) → β i}
:
(WithLp.equiv p ((i : ι) → β i)) (x + y) = (WithLp.equiv p ((i : ι) → β i)) x + (WithLp.equiv p ((i : ι) → β i)) y
@[simp]
theorem
PiLp.equiv_symm_add'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
{x : (i : ι) → β i}
{y : (i : ι) → β i}
:
(WithLp.equiv p ((i : ι) → β i)).symm (x + y) = (WithLp.equiv p ((i : ι) → β i)).symm x + (WithLp.equiv p ((i : ι) → β i)).symm y
@[simp]
theorem
PiLp.equiv_sub'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
{x : (i : ι) → β i}
{y : (i : ι) → β i}
:
(WithLp.equiv p ((i : ι) → β i)) (x - y) = (WithLp.equiv p ((i : ι) → β i)) x - (WithLp.equiv p ((i : ι) → β i)) y
@[simp]
theorem
PiLp.equiv_symm_sub'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
{x : (i : ι) → β i}
{y : (i : ι) → β i}
:
(WithLp.equiv p ((i : ι) → β i)).symm (x - y) = (WithLp.equiv p ((i : ι) → β i)).symm x - (WithLp.equiv p ((i : ι) → β i)).symm y
@[simp]
theorem
PiLp.equiv_neg'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
{x : (i : ι) → β i}
:
(WithLp.equiv p ((i : ι) → β i)) (-x) = -(WithLp.equiv p ((i : ι) → β i)) x
@[simp]
theorem
PiLp.equiv_symm_neg'
{ι : Type u_1}
{β : ι → Type u_2}
[(i : ι) → NormedAddCommGroup (β i)]
{p : ENNReal}
{x : (i : ι) → β i}
:
(WithLp.equiv p ((i : ι) → β i)).symm (-x) = -(WithLp.equiv p ((i : ι) → β i)).symm x