Product of normed groups and other constructions

This file constructs the infinity norm on finite products of normed groups and provides instances for type synonyms.

PUnit

@[implicit_reducible]

instance PUnit.normedAddCommGroup : NormedAddCommGroup PUnit.{u_5 + 1}

@[simp]

theorem PUnit.norm_eq_zero (x : PUnit.{u_5 + 1}) : ‖x‖ = 0

ULift

@[implicit_reducible]

instance ULift.norm {E : Type u_2} [Norm E] : Norm (ULift.{u_5, u_2} E)

theorem ULift.norm_def {E : Type u_2} [Norm E] (x : ULift.{u_5, u_2} E) : ‖x‖ = ‖x.down‖

@[simp]

theorem ULift.norm_up {E : Type u_2} [Norm E] (x : E) : ‖{ down := x }‖ = ‖x‖

@[simp]

theorem ULift.norm_down {E : Type u_2} [Norm E] (x : ULift.{u_5, u_2} E) : ‖x.down‖ = ‖x‖

@[implicit_reducible]

instance ULift.nnnorm {E : Type u_2} [NNNorm E] : NNNorm (ULift.{u_5, u_2} E)

theorem ULift.nnnorm_def {E : Type u_2} [NNNorm E] (x : ULift.{u_5, u_2} E) : ‖x‖₊ = ‖x.down‖₊

@[simp]

theorem ULift.nnnorm_up {E : Type u_2} [NNNorm E] (x : E) : ‖{ down := x }‖₊ = ‖x‖₊

@[simp]

theorem ULift.nnnorm_down {E : Type u_2} [NNNorm E] (x : ULift.{u_5, u_2} E) : ‖x.down‖₊ = ‖x‖₊

@[implicit_reducible]

instance ULift.seminormedGroup {E : Type u_2} [SeminormedGroup E] : SeminormedGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.seminormedAddGroup {E : Type u_2} [SeminormedAddGroup E] : SeminormedAddGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.seminormedCommGroup {E : Type u_2} [SeminormedCommGroup E] : SeminormedCommGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.seminormedAddCommGroup {E : Type u_2} [SeminormedAddCommGroup E] : SeminormedAddCommGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.normedGroup {E : Type u_2} [NormedGroup E] : NormedGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.normedAddGroup {E : Type u_2} [NormedAddGroup E] : NormedAddGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.normedCommGroup {E : Type u_2} [NormedCommGroup E] : NormedCommGroup (ULift.{u_5, u_2} E)

@[implicit_reducible]

instance ULift.normedAddCommGroup {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup (ULift.{u_5, u_2} E)

Additive, Multiplicative

@[implicit_reducible]

instance Additive.toNorm {E : Type u_2} [Norm E] : Norm (Additive E)

@[implicit_reducible]

instance Multiplicative.toNorm {E : Type u_2} [Norm E] : Norm (Multiplicative E)

@[simp]

theorem norm_toMul {E : Type u_2} [Norm E] (x : Additive E) : ‖Additive.toMul x‖ = ‖x‖

@[simp]

theorem norm_ofMul {E : Type u_2} [Norm E] (x : E) : ‖Additive.ofMul x‖ = ‖x‖

@[simp]

theorem norm_toAdd {E : Type u_2} [Norm E] (x : Multiplicative E) : ‖Multiplicative.toAdd x‖ = ‖x‖

@[simp]

theorem norm_ofAdd {E : Type u_2} [Norm E] (x : E) : ‖Multiplicative.ofAdd x‖ = ‖x‖

@[implicit_reducible]

instance Additive.toNNNorm {E : Type u_2} [NNNorm E] : NNNorm (Additive E)

@[implicit_reducible]

instance Multiplicative.toNNNorm {E : Type u_2} [NNNorm E] : NNNorm (Multiplicative E)

@[simp]

theorem nnnorm_toMul {E : Type u_2} [NNNorm E] (x : Additive E) : ‖Additive.toMul x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_ofMul {E : Type u_2} [NNNorm E] (x : E) : ‖Additive.ofMul x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_toAdd {E : Type u_2} [NNNorm E] (x : Multiplicative E) : ‖Multiplicative.toAdd x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_ofAdd {E : Type u_2} [NNNorm E] (x : E) : ‖Multiplicative.ofAdd x‖₊ = ‖x‖₊

@[implicit_reducible]

instance Additive.seminormedAddGroup {E : Type u_2} [SeminormedGroup E] : SeminormedAddGroup (Additive E)

@[implicit_reducible]

instance Multiplicative.seminormedGroup {E : Type u_2} [SeminormedAddGroup E] : SeminormedGroup (Multiplicative E)

@[implicit_reducible]

instance Additive.seminormedCommGroup {E : Type u_2} [SeminormedCommGroup E] : SeminormedAddCommGroup (Additive E)

@[implicit_reducible]

instance Multiplicative.seminormedAddCommGroup {E : Type u_2} [SeminormedAddCommGroup E] : SeminormedCommGroup (Multiplicative E)

@[implicit_reducible]

instance Additive.normedAddGroup {E : Type u_2} [NormedGroup E] : NormedAddGroup (Additive E)

@[implicit_reducible]

instance Multiplicative.normedGroup {E : Type u_2} [NormedAddGroup E] : NormedGroup (Multiplicative E)

@[implicit_reducible]

instance Additive.normedAddCommGroup {E : Type u_2} [NormedCommGroup E] : NormedAddCommGroup (Additive E)

@[implicit_reducible]

instance Multiplicative.normedCommGroup {E : Type u_2} [NormedAddCommGroup E] : NormedCommGroup (Multiplicative E)

Order dual

@[implicit_reducible]

instance OrderDual.toNorm {E : Type u_2} [Norm E] : Norm Eᵒᵈ

@[simp]

theorem norm_toDual {E : Type u_2} [Norm E] (x : E) : ‖OrderDual.toDual x‖ = ‖x‖

@[simp]

theorem norm_ofDual {E : Type u_2} [Norm E] (x : Eᵒᵈ) : ‖OrderDual.ofDual x‖ = ‖x‖

@[implicit_reducible]

instance OrderDual.toNNNorm {E : Type u_2} [NNNorm E] : NNNorm Eᵒᵈ

@[simp]

theorem nnnorm_toDual {E : Type u_2} [NNNorm E] (x : E) : ‖OrderDual.toDual x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_ofDual {E : Type u_2} [NNNorm E] (x : Eᵒᵈ) : ‖OrderDual.ofDual x‖₊ = ‖x‖₊

@[implicit_reducible, instance 100]

instance OrderDual.seminormedGroup {E : Type u_2} [SeminormedGroup E] : SeminormedGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.seminormedAddGroup {E : Type u_2} [SeminormedAddGroup E] : SeminormedAddGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.seminormedCommGroup {E : Type u_2} [SeminormedCommGroup E] : SeminormedCommGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.seminormedAddCommGroup {E : Type u_2} [SeminormedAddCommGroup E] : SeminormedAddCommGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.normedGroup {E : Type u_2} [NormedGroup E] : NormedGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.normedAddGroup {E : Type u_2} [NormedAddGroup E] : NormedAddGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.normedCommGroup {E : Type u_2} [NormedCommGroup E] : NormedCommGroup Eᵒᵈ

@[implicit_reducible, instance 100]

instance OrderDual.normedAddCommGroup {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup Eᵒᵈ

Binary product of normed groups

@[implicit_reducible]

instance Prod.toNorm {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] : Norm (E × F)

theorem Prod.norm_def {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖

@[simp]

theorem Prod.norm_mk {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E) (y : F) : ‖(x, y)‖ = max ‖x‖ ‖y‖

theorem norm_fst_le {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E × F) : ‖x.1‖ ≤ ‖x‖

theorem norm_snd_le {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E × F) : ‖x.2‖ ≤ ‖x‖

theorem norm_prod_le_iff {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] {x : E × F} {r : ℝ} : ‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r

@[implicit_reducible]

instance Prod.seminormedGroup {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] : SeminormedGroup (E × F)

Product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Prod.seminormedAddGroup {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] : SeminormedAddGroup (E × F)

Product of seminormed groups, using the sup norm.

theorem Prod.nnnorm_def' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

Multiplicative version of Prod.nnnorm_def. Earlier, this name was used for the additive version.

theorem Prod.nnnorm_def {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

@[simp]

theorem Prod.nnnorm_mk' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊

Multiplicative version of Prod.nnnorm_mk.

@[simp]

theorem Prod.nnnorm_mk {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊

@[implicit_reducible]

instance Prod.seminormedCommGroup {E : Type u_2} {F : Type u_3} [SeminormedCommGroup E] [SeminormedCommGroup F] : SeminormedCommGroup (E × F)

Product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Prod.seminormedAddCommGroup {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] : SeminormedAddCommGroup (E × F)

Product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Prod.normedGroup {E : Type u_2} {F : Type u_3} [NormedGroup E] [NormedGroup F] : NormedGroup (E × F)

Product of normed groups, using the sup norm.

@[implicit_reducible]

instance Prod.normedAddGroup {E : Type u_2} {F : Type u_3} [NormedAddGroup E] [NormedAddGroup F] : NormedAddGroup (E × F)

Product of normed groups, using the sup norm.

@[implicit_reducible]

instance Prod.normedCommGroup {E : Type u_2} {F : Type u_3} [NormedCommGroup E] [NormedCommGroup F] : NormedCommGroup (E × F)

Product of normed groups, using the sup norm.

@[implicit_reducible]

instance Prod.normedAddCommGroup {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] : NormedAddCommGroup (E × F)

Product of normed groups, using the sup norm.

Finite product of normed groups

@[implicit_reducible]

instance Pi.seminormedGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] : SeminormedGroup ((i : ι) → G i)

Finite product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Pi.seminormedAddGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] : SeminormedAddGroup ((i : ι) → G i)

Finite product of seminormed groups, using the sup norm.

theorem Pi.norm_def' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) : ‖f‖ = ↑(Finset.univ.sup fun (b : ι) => ‖f b‖₊)

theorem Pi.norm_def {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) : ‖f‖ = ↑(Finset.univ.sup fun (b : ι) => ‖f b‖₊)

theorem Pi.nnnorm_def' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) : ‖f‖₊ = Finset.univ.sup fun (b : ι) => ‖f b‖₊

theorem Pi.nnnorm_def {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) : ‖f‖₊ = Finset.univ.sup fun (b : ι) => ‖f b‖₊

theorem pi_norm_le_iff_of_nonneg' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : ℝ} (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

theorem pi_norm_le_iff_of_nonneg {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : ℝ} (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

theorem pi_nnnorm_le_iff' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : NNReal} : ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

theorem pi_nnnorm_le_iff {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : NNReal} : ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

theorem pi_norm_le_iff_of_nonempty' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) {r : ℝ} [Nonempty ι] : ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

theorem pi_norm_le_iff_of_nonempty {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) {r : ℝ} [Nonempty ι] : ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

theorem pi_norm_lt_iff' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : ℝ} (hr : 0 < r) : ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

theorem pi_norm_lt_iff {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : ℝ} (hr : 0 < r) : ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

theorem pi_nnnorm_lt_iff' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : NNReal} (hr : 0 < r) : ‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

theorem pi_nnnorm_lt_iff {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : NNReal} (hr : 0 < r) : ‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

theorem norm_le_pi_norm' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) (i : ι) : ‖f i‖ ≤ ‖f‖

theorem norm_le_pi_norm {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) (i : ι) : ‖f i‖ ≤ ‖f‖

theorem nnnorm_le_pi_nnnorm' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) (i : ι) : ‖f i‖₊ ≤ ‖f‖₊

theorem nnnorm_le_pi_nnnorm {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) (i : ι) : ‖f i‖₊ ≤ ‖f‖₊

theorem pi_norm_const_le' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] (a : E) : ‖fun (x : ι) => a‖ ≤ ‖a‖

theorem pi_norm_const_le {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] (a : E) : ‖fun (x : ι) => a‖ ≤ ‖a‖

theorem pi_nnnorm_const_le' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] (a : E) : ‖fun (x : ι) => a‖₊ ≤ ‖a‖₊

theorem pi_nnnorm_const_le {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] (a : E) : ‖fun (x : ι) => a‖₊ ≤ ‖a‖₊

@[simp]

theorem pi_norm_const' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖ = ‖a‖

@[simp]

theorem pi_norm_const {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖ = ‖a‖

@[simp]

theorem pi_nnnorm_const' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖₊ = ‖a‖₊

@[simp]

theorem pi_nnnorm_const {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖₊ = ‖a‖₊

theorem Pi.sum_norm_apply_le_norm' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) : ∑ i : ι, ‖f i‖ ≤ Fintype.card ι • ‖f‖

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.sum_norm_apply_le_norm {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) : ∑ i : ι, ‖f i‖ ≤ Fintype.card ι • ‖f‖

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.sum_nnnorm_apply_le_nnnorm' {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) : ∑ i : ι, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) : ∑ i : ι, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

@[implicit_reducible]

instance Pi.seminormedCommGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedCommGroup (G i)] : SeminormedCommGroup ((i : ι) → G i)

Finite product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Pi.seminormedAddCommGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (G i)] : SeminormedAddCommGroup ((i : ι) → G i)

Finite product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Pi.normedGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → NormedGroup (G i)] : NormedGroup ((i : ι) → G i)

Finite product of normed groups, using the sup norm.

@[implicit_reducible]

instance Pi.normedAddGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → NormedAddGroup (G i)] : NormedAddGroup ((i : ι) → G i)

Finite product of seminormed groups, using the sup norm.

@[implicit_reducible]

instance Pi.normedCommGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → NormedCommGroup (G i)] : NormedCommGroup ((i : ι) → G i)

Finite product of normed groups, using the sup norm.

@[implicit_reducible]

instance Pi.normedAddCommGroup {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [(i : ι) → NormedAddCommGroup (G i)] : NormedAddCommGroup ((i : ι) → G i)

Finite product of seminormed groups, using the sup norm.

theorem Pi.nnnorm_single {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖single i y‖₊ = ‖y‖₊

theorem Pi.enorm_single {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖single i y‖ₑ = ‖y‖ₑ

theorem Pi.norm_single {ι : Type u_1} {G : ι → Type u_4} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖single i y‖ = ‖y‖

Multiplicative opposite

@[implicit_reducible]

instance MulOpposite.instSeminormedAddGroup {E : Type u_2} [SeminormedAddGroup E] : SeminormedAddGroup Eᵐᵒᵖ

The (additive) norm on the multiplicative opposite is the same as the norm on the original type.

Note that we do not provide this more generally as Norm Eᵐᵒᵖ, as this is not always a good choice of norm in the multiplicative SeminormedGroup E case.

We could repeat this instance to provide a [SeminormedGroup E] : SeminormedGroup Eᵃᵒᵖ instance, but that case would likely never be used.

theorem MulOpposite.norm_op {E : Type u_2} [SeminormedAddGroup E] (a : E) : ‖op a‖ = ‖a‖

theorem MulOpposite.norm_unop {E : Type u_2} [SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖unop a‖ = ‖a‖

theorem MulOpposite.nnnorm_op {E : Type u_2} [SeminormedAddGroup E] (a : E) : ‖op a‖₊ = ‖a‖₊

theorem MulOpposite.nnnorm_unop {E : Type u_2} [SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖unop a‖₊ = ‖a‖₊

@[implicit_reducible]

instance MulOpposite.instNormedAddGroup {E : Type u_2} [NormedAddGroup E] : NormedAddGroup Eᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instSeminormedAddCommGroup {E : Type u_2} [SeminormedAddCommGroup E] : SeminormedAddCommGroup Eᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instNormedAddCommGroup {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup Eᵐᵒᵖ