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

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

ULift

@[instance_reducible]

instance ULift.norm {E : Type u_3} [Norm E] : Norm (ULift.{u_6, u_3} E)

Equations

• ULift.norm = { norm := fun (x : ULift.{?u.1, ?u.2} E) => ‖x.down‖ }

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

@[simp]

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

@[simp]

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

@[instance_reducible]

instance ULift.nnNorm {E : Type u_3} [NNNorm E] : NNNorm (ULift.{u_6, u_3} E)

Equations

• ULift.nnNorm = { nnNorm := fun (x : ULift.{?u.1, ?u.2} E) => ‖x.down‖₊ }

theorem ULift.nnNorm_def {E : Type u_3} [NNNorm E] (x : ULift.{u_6, u_3} E) : ‖x‖₊ = ‖x.down‖₊

@[deprecated ULift.nnNorm_def (since := "2026-10-31")]

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

Alias of ULift.nnNorm_def.

@[simp]

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

@[deprecated ULift.nnNorm_up (since := "2026-10-31")]

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

Alias of ULift.nnNorm_up.

@[simp]

theorem ULift.nnNorm_down {E : Type u_3} [NNNorm E] (x : ULift.{u_6, u_3} E) : ‖x.down‖₊ = ‖x‖₊

@[deprecated ULift.nnNorm_down (since := "2026-10-31")]

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

Alias of ULift.nnNorm_down.

@[instance_reducible]

instance ULift.seminormedGroup {E : Type u_3} [SeminormedGroup E] : SeminormedGroup (ULift.{u_6, u_3} E)

Equations

• ULift.seminormedGroup = SeminormedGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ }

@[instance_reducible]

instance ULift.seminormedAddGroup {E : Type u_3} [SeminormedAddGroup E] : SeminormedAddGroup (ULift.{u_6, u_3} E)

Equations

• ULift.seminormedAddGroup = SeminormedAddGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

instance ULift.seminormedCommGroup {E : Type u_3} [SeminormedCommGroup E] : SeminormedCommGroup (ULift.{u_6, u_3} E)

Equations

• ULift.seminormedCommGroup = SeminormedCommGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ }

@[instance_reducible]

instance ULift.seminormedAddCommGroup {E : Type u_3} [SeminormedAddCommGroup E] : SeminormedAddCommGroup (ULift.{u_6, u_3} E)

Equations

• ULift.seminormedAddCommGroup = SeminormedAddCommGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

instance ULift.normedGroup {E : Type u_3} [NormedGroup E] : NormedGroup (ULift.{u_6, u_3} E)

Equations

• ULift.normedGroup = NormedGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ } ⋯

@[instance_reducible]

instance ULift.normedAddGroup {E : Type u_3} [NormedAddGroup E] : NormedAddGroup (ULift.{u_6, u_3} E)

Equations

• ULift.normedAddGroup = NormedAddGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ } ⋯

@[instance_reducible]

instance ULift.normedCommGroup {E : Type u_3} [NormedCommGroup E] : NormedCommGroup (ULift.{u_6, u_3} E)

Equations

• ULift.normedCommGroup = NormedCommGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ } ⋯

@[instance_reducible]

instance ULift.normedAddCommGroup {E : Type u_3} [NormedAddCommGroup E] : NormedAddCommGroup (ULift.{u_6, u_3} E)

Equations

• ULift.normedAddCommGroup = NormedAddCommGroup.induced (ULift.{?u.1, ?u.2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ } ⋯

Additive, Multiplicative

@[instance_reducible]

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

Equations

• Additive.toNorm = inst✝

@[instance_reducible]

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

Equations

• Multiplicative.toNorm = inst✝

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

• Additive.toNNNorm = inst✝

@[instance_reducible]

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

Equations

• Multiplicative.toNNNorm = inst✝

@[simp]

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

@[deprecated nnNorm_toMul (since := "2026-10-31")]

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

Alias of nnNorm_toMul.

@[simp]

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

@[deprecated nnNorm_ofMul (since := "2026-10-31")]

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

Alias of nnNorm_ofMul.

@[simp]

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

@[deprecated nnNorm_toAdd (since := "2026-10-31")]

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

Alias of nnNorm_toAdd.

@[simp]

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

@[deprecated nnNorm_ofAdd (since := "2026-10-31")]

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

Alias of nnNorm_ofAdd.

@[instance_reducible]

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

Equations

• Additive.seminormedAddGroup = { toNorm := Additive.toNorm, toAddGroup := Additive.addGroup, toPseudoMetricSpace := instPseudoMetricSpaceAdditive, dist_eq := ⋯ }

@[instance_reducible]

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

Equations

• Multiplicative.seminormedGroup = { toNorm := Multiplicative.toNorm, toGroup := Multiplicative.group, toPseudoMetricSpace := instPseudoMetricSpaceMultiplicative, dist_eq := ⋯ }

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

Order dual

@[instance_reducible]

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

Equations

• OrderDual.toNorm = { norm := fun (x : Eᵒᵈ) => ‖OrderDual.ofDual x‖ }

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

• OrderDual.toNNNorm = { nnNorm := fun (x : Eᵒᵈ) => ‖OrderDual.ofDual x‖₊ }

@[simp]

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

@[deprecated nnNorm_toDual (since := "2026-10-31")]

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

Alias of nnNorm_toDual.

@[simp]

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

@[deprecated nnNorm_ofDual (since := "2026-10-31")]

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

Alias of nnNorm_ofDual.

@[instance_reducible, instance 100]

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

Equations

• OrderDual.seminormedGroup = { toNorm := OrderDual.toNorm, toGroup := OrderDual.instGroup, toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.seminormedAddGroup = { toNorm := OrderDual.toNorm, toAddGroup := OrderDual.instAddGroup, toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.seminormedCommGroup = { toNorm := OrderDual.toNorm, toCommGroup := OrderDual.instCommGroup, toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.seminormedAddCommGroup = { toNorm := OrderDual.toNorm, toAddCommGroup := OrderDual.instAddCommGroup, toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.normedGroup = { toNorm := OrderDual.toNorm, toGroup := OrderDual.instGroup, toMetricSpace := instMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.normedAddGroup = { toNorm := OrderDual.toNorm, toAddGroup := OrderDual.instAddGroup, toMetricSpace := instMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.normedCommGroup = { toNorm := OrderDual.toNorm, toCommGroup := OrderDual.instCommGroup, toMetricSpace := instMetricSpaceOrderDual, dist_eq := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• OrderDual.normedAddCommGroup = { toNorm := OrderDual.toNorm, toAddCommGroup := OrderDual.instAddCommGroup, toMetricSpace := instMetricSpaceOrderDual, dist_eq := ⋯ }

Binary product of normed groups

@[instance_reducible]

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

Equations

• Prod.toNorm = { norm := fun (x : E × F) => max ‖x.1‖ ‖x.2‖ }

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

@[simp]

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

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

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

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

@[instance_reducible]

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

Product of seminormed groups, using the sup norm.

Equations

• Prod.seminormedGroup = { toNorm := Prod.toNorm, toGroup := Prod.instGroup, toPseudoMetricSpace := Prod.pseudoMetricSpaceMax, dist_eq := ⋯ }

@[instance_reducible]

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

Product of seminormed groups, using the sup norm.

Equations

• Prod.seminormedAddGroup = { toNorm := Prod.toNorm, toAddGroup := Prod.instAddGroup, toPseudoMetricSpace := Prod.pseudoMetricSpaceMax, dist_eq := ⋯ }

theorem Prod.nnNorm_def' {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

Additive version of Prod.nnNorm_def'. Earlier, this name was used for the multiplicative version.

@[deprecated Prod.nnNorm_def' (since := "2026-10-31")]

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

Alias of Prod.nnNorm_def'.

---

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

@[deprecated Prod.nnNorm_def (since := "2026-10-31")]

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

Alias of Prod.nnNorm_def.

---

Additive version of Prod.nnNorm_def'. Earlier, this name was used for the multiplicative version.

@[simp]

theorem Prod.nnNorm_mk' {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊

Additive version of Prod.nnNorm_mk'.

@[deprecated Prod.nnNorm_mk' (since := "2026-10-31")]

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

Alias of Prod.nnNorm_mk'.

---

Multiplicative version of Prod.nnNorm_mk.

@[deprecated Prod.nnNorm_mk (since := "2026-10-31")]

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

Alias of Prod.nnNorm_mk.

---

Additive version of Prod.nnNorm_mk'.

@[instance_reducible]

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

Product of seminormed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Product of seminormed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Product of normed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Product of normed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Product of normed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Product of normed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

Finite product of normed groups

@[instance_reducible]

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

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.seminormedGroup = { norm := fun (f : (i : ι) → G i) => ↑(Finset.univ.sup fun (b : ι) => ‖f b‖₊), toGroup := Pi.group, toPseudoMetricSpace := pseudoMetricSpacePi, dist_eq := ⋯ }

@[instance_reducible]

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

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.seminormedAddGroup = { norm := fun (f : (i : ι) → G i) => ↑(Finset.univ.sup fun (b : ι) => ‖f b‖₊), toAddGroup := Pi.addGroup, toPseudoMetricSpace := pseudoMetricSpacePi, dist_eq := ⋯ }

theorem Pi.norm_def' {ι : Type u_1} {G : ι → Type u_5} [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_5} [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_5} [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_5} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) : ‖f‖₊ = Finset.univ.sup fun (b : ι) => ‖f b‖₊

@[deprecated Pi.nnNorm_def' (since := "2026-10-31")]

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

Alias of Pi.nnNorm_def'.

@[deprecated Pi.nnNorm_def (since := "2026-10-31")]

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

Alias of Pi.nnNorm_def.

theorem pi_norm_le_iff_of_nonneg' {ι : Type u_1} {G : ι → Type u_5} [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_5} [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_5} [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_5} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : NNReal} : ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

@[deprecated pi_nnNorm_le_iff' (since := "2026-10-31")]

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

Alias of pi_nnNorm_le_iff'.

@[deprecated pi_nnNorm_le_iff (since := "2026-10-31")]

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

Alias of pi_nnNorm_le_iff.

theorem pi_norm_le_iff_of_nonempty' {ι : Type u_1} {G : ι → Type u_5} [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_5} [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_5} [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_5} [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_5} [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_5} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : NNReal} (hr : 0 < r) : ‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

@[deprecated pi_nnNorm_lt_iff' (since := "2026-10-31")]

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

Alias of pi_nnNorm_lt_iff'.

@[deprecated pi_nnNorm_lt_iff (since := "2026-10-31")]

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

Alias of pi_nnNorm_lt_iff.

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

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

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

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

@[deprecated nnNorm_le_pi_nnNorm' (since := "2026-10-31")]

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

Alias of nnNorm_le_pi_nnNorm'.

@[deprecated nnNorm_le_pi_nnNorm (since := "2026-10-31")]

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

Alias of nnNorm_le_pi_nnNorm.

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

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

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

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

@[deprecated pi_nnNorm_const_le' (since := "2026-10-31")]

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

Alias of pi_nnNorm_const_le'.

@[deprecated pi_nnNorm_const_le (since := "2026-10-31")]

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

Alias of pi_nnNorm_const_le.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated pi_nnNorm_const' (since := "2026-10-31")]

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

Alias of pi_nnNorm_const'.

@[deprecated pi_nnNorm_const (since := "2026-10-31")]

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

Alias of pi_nnNorm_const.

theorem pi_nnNorm_comp_le' {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedGroup E] [Fintype F] (g : ι → E) (f : F → ι) : ‖g ∘ f‖₊ ≤ ‖g‖₊

theorem pi_nnNorm_comp_le {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedAddGroup E] [Fintype F] (g : ι → E) (f : F → ι) : ‖g ∘ f‖₊ ≤ ‖g‖₊

@[deprecated pi_nnNorm_comp_le' (since := "2026-10-31")]

theorem pi_nnnorm_comp_le' {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedGroup E] [Fintype F] (g : ι → E) (f : F → ι) : ‖g ∘ f‖₊ ≤ ‖g‖₊

Alias of pi_nnNorm_comp_le'.

@[deprecated pi_nnNorm_comp_le (since := "2026-10-31")]

theorem pi_nnnorm_comp_le {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedAddGroup E] [Fintype F] (g : ι → E) (f : F → ι) : ‖g ∘ f‖₊ ≤ ‖g‖₊

Alias of pi_nnNorm_comp_le.

theorem pi_norm_comp_le' {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedGroup E] [Fintype F] (g : ι → E) (f : F → ι) : ‖g ∘ f‖ ≤ ‖g‖

theorem pi_norm_comp_le {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedAddGroup E] [Fintype F] (g : ι → E) (f : F → ι) : ‖g ∘ f‖ ≤ ‖g‖

theorem IsGreatest.pi_norm' {ι : Type u_1} {E : Type u_3} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (f : ι → E) : IsGreatest (Set.range fun (x : ι) => ‖f x‖) ‖f‖

theorem IsGreatest.pi_norm {ι : Type u_1} {E : Type u_3} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (f : ι → E) : IsGreatest (Set.range fun (x : ι) => ‖f x‖) ‖f‖

theorem Function.Surjective.pi_norm_comp' {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedGroup E] [Fintype F] {f : ι → F} (hf : Surjective f) (g : F → E) : ‖g ∘ f‖ = ‖g‖

theorem Function.Surjective.pi_norm_comp {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [SeminormedAddGroup E] [Fintype F] {f : ι → F} (hf : Surjective f) (g : F → E) : ‖g ∘ f‖ = ‖g‖

theorem Pi.sum_norm_apply_le_norm' {ι : Type u_1} {G : ι → Type u_5} [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_5} [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_5} [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_5} [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.

@[deprecated Pi.sum_nnNorm_apply_le_nnNorm' (since := "2026-10-31")]

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

Alias of Pi.sum_nnNorm_apply_le_nnNorm'.

---

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

@[deprecated Pi.sum_nnNorm_apply_le_nnNorm (since := "2026-10-31")]

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

Alias of Pi.sum_nnNorm_apply_le_nnNorm.

---

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

theorem Pi.nnNorm_extend_le' {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] (f : ι → ι') (g : ι → E) (j : ι' → E) : ‖Function.extend f g j‖₊ ≤ max ‖g‖₊ ‖j‖₊

theorem Pi.nnNorm_extend_le {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] (f : ι → ι') (g : ι → E) (j : ι' → E) : ‖Function.extend f g j‖₊ ≤ max ‖g‖₊ ‖j‖₊

@[deprecated Pi.nnNorm_extend_le' (since := "2026-10-31")]

theorem Pi.nnnorm_extend_le' {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] (f : ι → ι') (g : ι → E) (j : ι' → E) : ‖Function.extend f g j‖₊ ≤ max ‖g‖₊ ‖j‖₊

Alias of Pi.nnNorm_extend_le'.

@[deprecated Pi.nnNorm_extend_le (since := "2026-10-31")]

theorem Pi.nnnorm_extend_le {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] (f : ι → ι') (g : ι → E) (j : ι' → E) : ‖Function.extend f g j‖₊ ≤ max ‖g‖₊ ‖j‖₊

Alias of Pi.nnNorm_extend_le.

theorem Pi.norm_extend_le' {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] (f : ι → ι') (g : ι → E) (j : ι' → E) : ‖Function.extend f g j‖ ≤ max ‖g‖ ‖j‖

theorem Pi.norm_extend_le {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] (f : ι → ι') (g : ι → E) (j : ι' → E) : ‖Function.extend f g j‖ ≤ max ‖g‖ ‖j‖

theorem Function.FactorsThrough.nnNorm_extend' {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] {f : ι → ι'} {g : ι → E} {j : ι' → E} (h : FactorsThrough g f) (hj : ‖j‖₊ ≤ ‖g‖₊) : ‖extend f g j‖₊ = ‖g‖₊

theorem Function.FactorsThrough.nnNorm_extend {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] {f : ι → ι'} {g : ι → E} {j : ι' → E} (h : FactorsThrough g f) (hj : ‖j‖₊ ≤ ‖g‖₊) : ‖extend f g j‖₊ = ‖g‖₊

@[deprecated Function.FactorsThrough.nnNorm_extend' (since := "2026-10-31")]

theorem Function.FactorsThrough.nnnorm_extend' {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] {f : ι → ι'} {g : ι → E} {j : ι' → E} (h : FactorsThrough g f) (hj : ‖j‖₊ ≤ ‖g‖₊) : ‖extend f g j‖₊ = ‖g‖₊

Alias of Function.FactorsThrough.nnNorm_extend'.

@[deprecated Function.FactorsThrough.nnNorm_extend (since := "2026-10-31")]

theorem Function.FactorsThrough.nnnorm_extend {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] {f : ι → ι'} {g : ι → E} {j : ι' → E} (h : FactorsThrough g f) (hj : ‖j‖₊ ≤ ‖g‖₊) : ‖extend f g j‖₊ = ‖g‖₊

Alias of Function.FactorsThrough.nnNorm_extend.

theorem Function.FactorsThrough.norm_extend' {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] {f : ι → ι'} {g : ι → E} {j : ι' → E} (h : FactorsThrough g f) (hj : ‖j‖ ≤ ‖g‖) : ‖extend f g j‖ = ‖g‖

theorem Function.FactorsThrough.norm_extend {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] {f : ι → ι'} {g : ι → E} {j : ι' → E} (h : FactorsThrough g f) (hj : ‖j‖ ≤ ‖g‖) : ‖extend f g j‖ = ‖g‖

theorem Function.FactorsThrough.nnNorm_extend_one {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] {f : ι → ι'} {g : ι → E} (h : FactorsThrough g f) : ‖extend f g 1‖₊ = ‖g‖₊

theorem Function.FactorsThrough.nnNorm_extend_zero {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] {f : ι → ι'} {g : ι → E} (h : FactorsThrough g f) : ‖extend f g 0‖₊ = ‖g‖₊

@[deprecated Function.FactorsThrough.nnNorm_extend_one (since := "2026-10-31")]

theorem Function.FactorsThrough.nnnorm_extend_one {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] {f : ι → ι'} {g : ι → E} (h : FactorsThrough g f) : ‖extend f g 1‖₊ = ‖g‖₊

Alias of Function.FactorsThrough.nnNorm_extend_one.

@[deprecated Function.FactorsThrough.nnNorm_extend_zero (since := "2026-10-31")]

theorem Function.FactorsThrough.nnnorm_extend_zero {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] {f : ι → ι'} {g : ι → E} (h : FactorsThrough g f) : ‖extend f g 0‖₊ = ‖g‖₊

Alias of Function.FactorsThrough.nnNorm_extend_zero.

theorem Function.FactorsThrough.norm_extend_one {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedGroup E] {f : ι → ι'} {g : ι → E} (h : FactorsThrough g f) : ‖extend f g 1‖ = ‖g‖

theorem Function.FactorsThrough.norm_extend_zero {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [SeminormedAddGroup E] {f : ι → ι'} {g : ι → E} (h : FactorsThrough g f) : ‖extend f g 0‖ = ‖g‖

@[instance_reducible]

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

Finite product of seminormed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Finite product of seminormed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Finite product of normed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Finite product of seminormed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Finite product of normed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Finite product of seminormed groups, using the sup norm.

Equations

• One or more equations did not get rendered due to their size.

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

@[deprecated Pi.nnNorm_single (since := "2026-10-31")]

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

Alias of Pi.nnNorm_single.

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

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

Multiplicative opposite

@[instance_reducible]

instance MulOpposite.instSeminormedAddGroup {E : Type u_3} [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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

@[deprecated MulOpposite.nnNorm_op (since := "2026-10-31")]

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

Alias of MulOpposite.nnNorm_op.

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

@[deprecated MulOpposite.nnNorm_unop (since := "2026-10-31")]

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

Alias of MulOpposite.nnNorm_unop.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.