Group seminorms

This file defines norms and seminorms in a group. A group seminorm is a function to the reals which is positive-semidefinite and subadditive. A norm further only maps zero to zero.

Main declarations

• AddGroupSeminorm: A function f from an additive group G to the reals that preserves zero, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.
• NonarchAddGroupSeminorm: A function f from an additive group G to the reals that preserves zero, takes nonnegative values, is nonarchimedean and such that f (-x) = f x for all x.
• GroupSeminorm: A function f from a group G to the reals that sends one to zero, takes nonnegative values, is submultiplicative and such that f x⁻¹ = f x for all x.
• AddGroupNorm: A seminorm f such that f x = 0 → x = 0 for all x.
• NonarchAddGroupNorm: A nonarchimedean seminorm f such that f x = 0 → x = 0 for all x.
• GroupNorm: A seminorm f such that f x = 0 → x = 1 for all x.

Notes

The corresponding hom classes are defined in Analysis.Order.Hom.Basic to be used by absolute values.

We do not define NonarchAddGroupSeminorm as an extension of AddGroupSeminorm to avoid having a superfluous add_le' field in the resulting structure. The same applies to NonarchAddGroupNorm.

References

• [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags

norm, seminorm

structure AddGroupSeminorm (G : Type u_7) [AddGroup G] : Type u_7

• toFun : G → ℝ

  The bare function of an AddGroupSeminorm.

• map_zero' : AddGroupSeminorm.toFun s 0 = 0

  The image of zero is zero.

• add_le' : ∀ (r s_1 : G), AddGroupSeminorm.toFun s (r + s_1) ≤ AddGroupSeminorm.toFun s r + AddGroupSeminorm.toFun s s_1

  The seminorm is subadditive.

• neg' : ∀ (r : G), AddGroupSeminorm.toFun s (-r) = AddGroupSeminorm.toFun s r

  The seminorm is invariant under negation.

A seminorm on an additive group G is a function f : G → ℝ that preserves zero, is subadditive and such that f (-x) = f x for all x.

structure GroupSeminorm (G : Type u_7) [Group G] : Type u_7

• toFun : G → ℝ

  The bare function of a GroupSeminorm.

• map_one' : GroupSeminorm.toFun s 1 = 0

  The image of one is zero.

• mul_le' : ∀ (x y : G), GroupSeminorm.toFun s (x * y) ≤ GroupSeminorm.toFun s x + GroupSeminorm.toFun s y

  The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.

• inv' : ∀ (x : G), GroupSeminorm.toFun s x⁻¹ = GroupSeminorm.toFun s x

  The seminorm is invariant under inversion.

A seminorm on a group G is a function f : G → ℝ that sends one to zero, is submultiplicative and such that f x⁻¹ = f x for all x.

structure NonarchAddGroupSeminorm (G : Type u_7) [AddGroup G] extends ZeroHom : Type u_7

• toFun : G → ℝ
• map_zero' : ZeroHom.toFun s.toZeroHom 0 = 0
• add_le_max' : ∀ (r s_1 : G), ZeroHom.toFun s.toZeroHom (r + s_1) ≤ max (ZeroHom.toFun s.toZeroHom r) (ZeroHom.toFun s.toZeroHom s_1)

  The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.

• neg' : ∀ (r : G), ZeroHom.toFun s.toZeroHom (-r) = ZeroHom.toFun s.toZeroHom r

  The seminorm is invariant under negation.

A nonarchimedean seminorm on an additive group G is a function f : G → ℝ that preserves zero, is nonarchimedean and such that f (-x) = f x for all x.

NOTE: We do not define NonarchAddGroupSeminorm as an extension of AddGroupSeminorm to avoid having a superfluous add_le' field in the resulting structure. The same applies to NonarchAddGroupNorm below.

structure AddGroupNorm (G : Type u_7) [AddGroup G] extends AddGroupSeminorm : Type u_7

• toFun : G → ℝ
• map_zero' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 0 = 0
• add_le' : ∀ (r s_1 : G), AddGroupSeminorm.toFun s.toAddGroupSeminorm (r + s_1) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm r + AddGroupSeminorm.toFun s.toAddGroupSeminorm s_1
• neg' : ∀ (r : G), AddGroupSeminorm.toFun s.toAddGroupSeminorm (-r) = AddGroupSeminorm.toFun s.toAddGroupSeminorm r
• eq_zero_of_map_eq_zero' : ∀ (x : G), AddGroupSeminorm.toFun s.toAddGroupSeminorm x = 0 → x = 0

  If the image under the seminorm is zero, then the argument is zero.

A norm on an additive group G is a function f : G → ℝ that preserves zero, is subadditive and such that f (-x) = f x and f x = 0 → x = 0 for all x.

structure GroupNorm (G : Type u_7) [Group G] extends GroupSeminorm : Type u_7

• toFun : G → ℝ
• map_one' : GroupSeminorm.toFun s.toGroupSeminorm 1 = 0
• mul_le' : ∀ (x y : G), GroupSeminorm.toFun s.toGroupSeminorm (x * y) ≤ GroupSeminorm.toFun s.toGroupSeminorm x + GroupSeminorm.toFun s.toGroupSeminorm y
• inv' : ∀ (x : G), GroupSeminorm.toFun s.toGroupSeminorm x⁻¹ = GroupSeminorm.toFun s.toGroupSeminorm x
• eq_one_of_map_eq_zero' : ∀ (x : G), GroupSeminorm.toFun s.toGroupSeminorm x = 0 → x = 1

  If the image under the norm is zero, then the argument is one.

A seminorm on a group G is a function f : G → ℝ that sends one to zero, is submultiplicative and such that f x⁻¹ = f x and f x = 0 → x = 1 for all x.

structure NonarchAddGroupNorm (G : Type u_7) [AddGroup G] extends NonarchAddGroupSeminorm : Type u_7

• toFun : G → ℝ
• map_zero' : ZeroHom.toFun s.toZeroHom 0 = 0
• add_le_max' : ∀ (r s_1 : G), ZeroHom.toFun s.toZeroHom (r + s_1) ≤ max (ZeroHom.toFun s.toZeroHom r) (ZeroHom.toFun s.toZeroHom s_1)
• neg' : ∀ (r : G), ZeroHom.toFun s.toZeroHom (-r) = ZeroHom.toFun s.toZeroHom r
• eq_zero_of_map_eq_zero' : ∀ (x : G), ZeroHom.toFun s.toZeroHom x = 0 → x = 0

  If the image under the norm is zero, then the argument is zero.

A nonarchimedean norm on an additive group G is a function f : G → ℝ that preserves zero, is nonarchimedean and such that f (-x) = f x and f x = 0 → x = 0 for all x.

class NonarchAddGroupSeminormClass (F : Type u_7) (α : outParam (Type u_8)) [AddGroup α] extends NonarchimedeanHomClass : Type (max u_7 u_8)

• coe : F → α → ℝ
• coe_injective' : Function.Injective FunLike.coe
• map_add_le_max : ∀ (f : F) (a b : α), ↑f (a + b) ≤ max (↑f a) (↑f b)
• map_zero : ∀ (f : F), ↑f 0 = 0

  The image of zero is zero.

• map_neg_eq_map' : ∀ (f : F) (a : α), ↑f (-a) = ↑f a

  The seminorm is invariant under negation.

NonarchAddGroupSeminormClass F α states that F is a type of nonarchimedean seminorms on the additive group α.

You should extend this class when you extend NonarchAddGroupSeminorm.

class NonarchAddGroupNormClass (F : Type u_7) (α : outParam (Type u_8)) [AddGroup α] extends NonarchAddGroupSeminormClass : Type (max u_7 u_8)

• coe : F → α → ℝ
• coe_injective' : Function.Injective FunLike.coe
• map_add_le_max : ∀ (f : F) (a b : α), ↑f (a + b) ≤ max (↑f a) (↑f b)
• map_zero : ∀ (f : F), ↑f 0 = 0
• map_neg_eq_map' : ∀ (f : F) (a : α), ↑f (-a) = ↑f a
• eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, ↑f a = 0 → a = 0

  If the image under the norm is zero, then the argument is zero.

NonarchAddGroupNormClass F α states that F is a type of nonarchimedean norms on the additive group α.

You should extend this class when you extend NonarchAddGroupNorm.

theorem map_sub_le_max {E : Type u_4} {F : Type u_5} [AddGroup E] [NonarchAddGroupSeminormClass F E] (f : F) (x : E) (y : E) : ↑f (x - y) ≤ max (↑f x) (↑f y)

instance NonarchAddGroupSeminormClass.toAddGroupSeminormClass {E : Type u_4} {F : Type u_5} [AddGroup E] [NonarchAddGroupSeminormClass F E] : AddGroupSeminormClass F E ℝ

instance NonarchAddGroupNormClass.toAddGroupNormClass {E : Type u_4} {F : Type u_5} [AddGroup E] [NonarchAddGroupNormClass F E] : AddGroupNormClass F E ℝ

Seminorms

instance AddGroupSeminorm.addGroupSeminormClass {E : Type u_4} [AddGroup E] : AddGroupSeminormClass (AddGroupSeminorm E) E ℝ

theorem AddGroupSeminorm.addGroupSeminormClass.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (g : AddGroupSeminorm E) (h : (fun f => f.toFun) f = (fun f => f.toFun) g) : f = g

instance GroupSeminorm.groupSeminormClass {E : Type u_4} [Group E] : GroupSeminormClass (GroupSeminorm E) E ℝ

instance AddGroupSeminorm.instCoeFunAddGroupSeminormForAllReal {E : Type u_4} [AddGroup E] : CoeFun (AddGroupSeminorm E) fun x => E → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

instance GroupSeminorm.instCoeFunGroupSeminormForAllReal {E : Type u_4} [Group E] : CoeFun (GroupSeminorm E) fun x => E → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

@[simp]

theorem AddGroupSeminorm.toFun_eq_coe {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} : p.toFun = ↑p

@[simp]

theorem GroupSeminorm.toFun_eq_coe {E : Type u_4} [Group E] {p : GroupSeminorm E} : p.toFun = ↑p

theorem AddGroupSeminorm.ext {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : (∀ (x : E), ↑p x = ↑q x) → p = q

theorem GroupSeminorm.ext {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : (∀ (x : E), ↑p x = ↑q x) → p = q

instance AddGroupSeminorm.instPartialOrderAddGroupSeminorm {E : Type u_4} [AddGroup E] : PartialOrder (AddGroupSeminorm E)

theorem AddGroupSeminorm.instPartialOrderAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun f => ↑f

instance GroupSeminorm.instPartialOrderGroupSeminorm {E : Type u_4} [Group E] : PartialOrder (GroupSeminorm E)

theorem AddGroupSeminorm.le_def {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : p ≤ q ↔ ↑p ≤ ↑q

theorem GroupSeminorm.le_def {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : p ≤ q ↔ ↑p ≤ ↑q

theorem AddGroupSeminorm.lt_def {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : p < q ↔ ↑p < ↑q

theorem GroupSeminorm.lt_def {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : p < q ↔ ↑p < ↑q

@[simp]

theorem AddGroupSeminorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : ↑p ≤ ↑q ↔ p ≤ q

@[simp]

theorem GroupSeminorm.coe_le_coe {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : ↑p ≤ ↑q ↔ p ≤ q

@[simp]

theorem AddGroupSeminorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : ↑p < ↑q ↔ p < q

@[simp]

theorem GroupSeminorm.coe_lt_coe {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : ↑p < ↑q ↔ p < q

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_2 {E : Type u_1} [AddGroup E] : ∀ (x x_1 : E), OfNat.ofNat 0 (x + x_1) ≤ 0 + OfNat.ofNat 0 (x + x_1)

instance AddGroupSeminorm.instZeroAddGroupSeminorm {E : Type u_4} [AddGroup E] : Zero (AddGroupSeminorm E)

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] : OfNat.ofNat 0 0 = 0

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_3 {E : Type u_1} [AddGroup E] : ∀ (x : E), OfNat.ofNat 0 (-x) = OfNat.ofNat 0 (-x)

instance GroupSeminorm.instZeroGroupSeminorm {E : Type u_4} [Group E] : Zero (GroupSeminorm E)

@[simp]

theorem AddGroupSeminorm.coe_zero {E : Type u_4} [AddGroup E] : ↑0 = 0

@[simp]

theorem GroupSeminorm.coe_zero {E : Type u_4} [Group E] : ↑0 = 0

@[simp]

theorem AddGroupSeminorm.zero_apply {E : Type u_4} [AddGroup E] (x : E) : ↑0 x = 0

@[simp]

theorem GroupSeminorm.zero_apply {E : Type u_4} [Group E] (x : E) : ↑0 x = 0

instance AddGroupSeminorm.instInhabitedAddGroupSeminorm {E : Type u_4} [AddGroup E] : Inhabited (AddGroupSeminorm E)

instance GroupSeminorm.instInhabitedGroupSeminorm {E : Type u_4} [Group E] : Inhabited (GroupSeminorm E)

theorem AddGroupSeminorm.instAddAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : (fun x => ↑p x + ↑q x) 0 = 0

theorem AddGroupSeminorm.instAddAddGroupSeminorm.proof_3 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : (fun x => ↑p x + ↑q x) (-x) = (fun x => ↑p x + ↑q x) x

theorem AddGroupSeminorm.instAddAddGroupSeminorm.proof_2 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ∀ (x x_1 : E), ↑p (x + x_1) + ↑q (x + x_1) ≤ (fun x => ↑p x + ↑q x) x + (fun x => ↑p x + ↑q x) x_1

instance AddGroupSeminorm.instAddAddGroupSeminorm {E : Type u_4} [AddGroup E] : Add (AddGroupSeminorm E)

instance GroupSeminorm.instAddGroupSeminorm {E : Type u_4} [Group E] : Add (GroupSeminorm E)

@[simp]

theorem AddGroupSeminorm.coe_add {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ↑(p + q) = ↑p + ↑q

@[simp]

theorem GroupSeminorm.coe_add {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) : ↑(p + q) = ↑p + ↑q

@[simp]

theorem AddGroupSeminorm.add_apply {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ↑(p + q) x = ↑p x + ↑q x

@[simp]

theorem GroupSeminorm.add_apply {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) (x : E) : ↑(p + q) x = ↑p x + ↑q x

instance AddGroupSeminorm.instSupAddGroupSeminorm {E : Type u_4} [AddGroup E] : Sup (AddGroupSeminorm E)

theorem AddGroupSeminorm.instSupAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : (↑p ⊔ ↑q) 0 = 0

theorem AddGroupSeminorm.instSupAddGroupSeminorm.proof_3 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : (↑p ⊔ ↑q) (-x) = (↑p ⊔ ↑q) x

theorem AddGroupSeminorm.instSupAddGroupSeminorm.proof_2 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) (y : E) : ↑p (x + y) ⊔ ↑q (x + y) ≤ (↑p ⊔ ↑q) x + (↑p ⊔ ↑q) y

instance GroupSeminorm.instSupGroupSeminorm {E : Type u_4} [Group E] : Sup (GroupSeminorm E)

@[simp]

theorem AddGroupSeminorm.coe_sup {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ↑(p ⊔ q) = ↑p ⊔ ↑q

@[simp]

theorem GroupSeminorm.coe_sup {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) : ↑(p ⊔ q) = ↑p ⊔ ↑q

@[simp]

theorem AddGroupSeminorm.sup_apply {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ↑(p ⊔ q) x = ↑p x ⊔ ↑q x

@[simp]

theorem GroupSeminorm.sup_apply {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) (x : E) : ↑(p ⊔ q) x = ↑p x ⊔ ↑q x

theorem AddGroupSeminorm.semilatticeSup.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun f => ↑f

instance AddGroupSeminorm.semilatticeSup {E : Type u_4} [AddGroup E] : SemilatticeSup (AddGroupSeminorm E)

instance GroupSeminorm.semilatticeSup {E : Type u_4} [Group E] : SemilatticeSup (GroupSeminorm E)

theorem AddGroupSeminorm.comp.proof_3 {E : Type u_1} {F : Type u_2} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) (x : F) : (fun x => ↑p (↑f x)) (-x) = (fun x => ↑p (↑f x)) x

theorem AddGroupSeminorm.comp.proof_1 {E : Type u_1} {F : Type u_2} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : (fun x => ↑p (↑f x)) 0 = 0

def AddGroupSeminorm.comp {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : AddGroupSeminorm F

Composition of an additive group seminorm with an additive monoid homomorphism as an additive group seminorm.

theorem AddGroupSeminorm.comp.proof_2 {E : Type u_1} {F : Type u_2} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : ∀ (x x_1 : F), ↑p (↑f (x + x_1)) ≤ (fun x => ↑p (↑f x)) x + (fun x => ↑p (↑f x)) x_1

def GroupSeminorm.comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) : GroupSeminorm F

Composition of a group seminorm with a monoid homomorphism as a group seminorm.

@[simp]

theorem AddGroupSeminorm.coe_comp {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : ↑(AddGroupSeminorm.comp p f) = ↑p ∘ ↑f

@[simp]

theorem GroupSeminorm.coe_comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) : ↑(GroupSeminorm.comp p f) = ↑p ∘ ↑f

@[simp]

theorem AddGroupSeminorm.comp_apply {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) (x : F) : ↑(AddGroupSeminorm.comp p f) x = ↑p (↑f x)

@[simp]

theorem GroupSeminorm.comp_apply {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) (x : F) : ↑(GroupSeminorm.comp p f) x = ↑p (↑f x)

@[simp]

theorem AddGroupSeminorm.comp_id {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) : AddGroupSeminorm.comp p (AddMonoidHom.id E) = p

@[simp]

theorem GroupSeminorm.comp_id {E : Type u_4} [Group E] (p : GroupSeminorm E) : GroupSeminorm.comp p (MonoidHom.id E) = p

@[simp]

theorem AddGroupSeminorm.comp_zero {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) : AddGroupSeminorm.comp p 0 = 0

@[simp]

theorem GroupSeminorm.comp_zero {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) : GroupSeminorm.comp p 1 = 0

@[simp]

theorem AddGroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (f : F →+ E) : AddGroupSeminorm.comp 0 f = 0

@[simp]

theorem GroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (f : F →* E) : GroupSeminorm.comp 0 f = 0

theorem AddGroupSeminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddGroup E] [AddGroup F] [AddGroup G] (p : AddGroupSeminorm E) (g : F →+ E) (f : G →+ F) : AddGroupSeminorm.comp p (AddMonoidHom.comp g f) = AddGroupSeminorm.comp (AddGroupSeminorm.comp p g) f

theorem GroupSeminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [Group E] [Group F] [Group G] (p : GroupSeminorm E) (g : F →* E) (f : G →* F) : GroupSeminorm.comp p (MonoidHom.comp g f) = GroupSeminorm.comp (GroupSeminorm.comp p g) f

theorem AddGroupSeminorm.add_comp {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (f : F →+ E) : AddGroupSeminorm.comp (p + q) f = AddGroupSeminorm.comp p f + AddGroupSeminorm.comp q f

theorem GroupSeminorm.add_comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) (q : GroupSeminorm E) (f : F →* E) : GroupSeminorm.comp (p + q) f = GroupSeminorm.comp p f + GroupSeminorm.comp q f

theorem AddGroupSeminorm.comp_mono {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} (f : F →+ E) (hp : p ≤ q) : AddGroupSeminorm.comp p f ≤ AddGroupSeminorm.comp q f

theorem GroupSeminorm.comp_mono {E : Type u_4} {F : Type u_5} [Group E] [Group F] {p : GroupSeminorm E} {q : GroupSeminorm E} (f : F →* E) (hp : p ≤ q) : GroupSeminorm.comp p f ≤ GroupSeminorm.comp q f

theorem AddGroupSeminorm.comp_add_le {E : Type u_4} {F : Type u_5} [AddCommGroup E] [AddCommGroup F] (p : AddGroupSeminorm E) (f : F →+ E) (g : F →+ E) : AddGroupSeminorm.comp p (f + g) ≤ AddGroupSeminorm.comp p f + AddGroupSeminorm.comp p g

theorem GroupSeminorm.comp_mul_le {E : Type u_4} {F : Type u_5} [CommGroup E] [CommGroup F] (p : GroupSeminorm E) (f : F →* E) (g : F →* E) : GroupSeminorm.comp p (f * g) ≤ GroupSeminorm.comp p f + GroupSeminorm.comp p g

theorem AddGroupSeminorm.add_bddBelow_range_add {E : Type u_4} [AddCommGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} {x : E} : BddBelow (Set.range fun y => ↑p y + ↑q (x - y))

theorem GroupSeminorm.mul_bddBelow_range_add {E : Type u_4} [CommGroup E] {p : GroupSeminorm E} {q : GroupSeminorm E} {x : E} : BddBelow (Set.range fun y => ↑p y + ↑q (x / y))

theorem AddGroupSeminorm.instInfAddGroupSeminormToAddGroup.proof_3 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ⨅ (y : E), ↑p y + ↑q (-x - y) = (fun x => ⨅ (y : E), ↑p y + ↑q (x - y)) x

theorem AddGroupSeminorm.instInfAddGroupSeminormToAddGroup.proof_2 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) (y : E) : (fun x => ⨅ (y : E), ↑p y + ↑q (x - y)) (x + y) ≤ (⨅ (y : E), ↑p y + ↑q (x - y)) + ⨅ (y : E), ↑p y + ↑q (y - y)

theorem AddGroupSeminorm.instInfAddGroupSeminormToAddGroup.proof_1 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ⨅ (i : E), ↑p i + ↑q (0 - i) = 0

noncomputable instance AddGroupSeminorm.instInfAddGroupSeminormToAddGroup {E : Type u_4} [AddCommGroup E] : Inf (AddGroupSeminorm E)

noncomputable instance GroupSeminorm.instInfGroupSeminormToGroup {E : Type u_4} [CommGroup E] : Inf (GroupSeminorm E)

@[simp]

theorem AddGroupSeminorm.inf_apply {E : Type u_4} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ↑(p ⊓ q) x = ⨅ (y : E), ↑p y + ↑q (x - y)

@[simp]

theorem GroupSeminorm.inf_apply {E : Type u_4} [CommGroup E] (p : GroupSeminorm E) (q : GroupSeminorm E) (x : E) : ↑(p ⊓ q) x = ⨅ (y : E), ↑p y + ↑q (x / y)

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : AddGroupSeminorm E) (b : AddGroupSeminorm E) : a ≤ a ⊔ b

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_3 {E : Type u_1} [AddCommGroup E] (a : AddGroupSeminorm E) (b : AddGroupSeminorm E) (c : AddGroupSeminorm E) : a ≤ c → b ≤ c → a ⊔ b ≤ c

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_4 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ⨅ (y : E), ↑p y + ↑q (x - y) ≤ (fun f => ↑f) p x

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_2 {E : Type u_1} [AddCommGroup E] (a : AddGroupSeminorm E) (b : AddGroupSeminorm E) : b ≤ a ⊔ b

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_5 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ⨅ (y : E), ↑p y + ↑q (x - y) ≤ (fun f => ↑f) q x

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_6 {E : Type u_1} [AddCommGroup E] (a : AddGroupSeminorm E) (b : AddGroupSeminorm E) (c : AddGroupSeminorm E) (hb : a ≤ b) (hc : a ≤ c) (x : E) : (fun f => ↑f) a x ≤ ⨅ (y : E), ↑b y + ↑c (x - y)

noncomputable instance AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup {E : Type u_4} [AddCommGroup E] : Lattice (AddGroupSeminorm E)

noncomputable instance GroupSeminorm.instLatticeGroupSeminormToGroup {E : Type u_4} [CommGroup E] : Lattice (GroupSeminorm E)

instance AddGroupSeminorm.toOne {E : Type u_4} [AddGroup E] [DecidableEq E] : One (AddGroupSeminorm E)

@[simp]

theorem AddGroupSeminorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) : ↑1 x = if x = 0 then 0 else 1

instance AddGroupSeminorm.toSMul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] : SMul R (AddGroupSeminorm E)

Any action on ℝ which factors through ℝ≥0 applies to an AddGroupSeminorm.

@[simp]

theorem AddGroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) : ↑(r • p) = r • ↑p

@[simp]

theorem AddGroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) (x : E) : ↑(r • p) x = r • ↑p x

instance AddGroupSeminorm.isScalarTower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (AddGroupSeminorm E)

theorem AddGroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

instance NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass {E : Type u_4} [AddGroup E] : NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E

instance NonarchAddGroupSeminorm.instCoeFunNonarchAddGroupSeminormForAllReal {E : Type u_4} [AddGroup E] : CoeFun (NonarchAddGroupSeminorm E) fun x => E → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

@[simp]

theorem NonarchAddGroupSeminorm.toZeroHom_eq_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} : ↑p.toZeroHom = ↑p

theorem NonarchAddGroupSeminorm.ext {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : (∀ (x : E), ↑p x = ↑q x) → p = q

noncomputable instance NonarchAddGroupSeminorm.instPartialOrderNonarchAddGroupSeminorm {E : Type u_4} [AddGroup E] : PartialOrder (NonarchAddGroupSeminorm E)

theorem NonarchAddGroupSeminorm.le_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : p ≤ q ↔ ↑p ≤ ↑q

theorem NonarchAddGroupSeminorm.lt_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : p < q ↔ ↑p < ↑q

@[simp]

theorem NonarchAddGroupSeminorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : ↑p ≤ ↑q ↔ p ≤ q

@[simp]

theorem NonarchAddGroupSeminorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : ↑p < ↑q ↔ p < q

instance NonarchAddGroupSeminorm.instZeroNonarchAddGroupSeminorm {E : Type u_4} [AddGroup E] : Zero (NonarchAddGroupSeminorm E)

@[simp]

theorem NonarchAddGroupSeminorm.coe_zero {E : Type u_4} [AddGroup E] : ↑0 = 0

@[simp]

theorem NonarchAddGroupSeminorm.zero_apply {E : Type u_4} [AddGroup E] (x : E) : ↑0 x = 0

instance NonarchAddGroupSeminorm.instInhabitedNonarchAddGroupSeminorm {E : Type u_4} [AddGroup E] : Inhabited (NonarchAddGroupSeminorm E)

instance NonarchAddGroupSeminorm.instSupNonarchAddGroupSeminorm {E : Type u_4} [AddGroup E] : Sup (NonarchAddGroupSeminorm E)

@[simp]

theorem NonarchAddGroupSeminorm.coe_sup {E : Type u_4} [AddGroup E] (p : NonarchAddGroupSeminorm E) (q : NonarchAddGroupSeminorm E) : ↑(p ⊔ q) = ↑p ⊔ ↑q

@[simp]

theorem NonarchAddGroupSeminorm.sup_apply {E : Type u_4} [AddGroup E] (p : NonarchAddGroupSeminorm E) (q : NonarchAddGroupSeminorm E) (x : E) : ↑(p ⊔ q) x = ↑p x ⊔ ↑q x

noncomputable instance NonarchAddGroupSeminorm.instSemilatticeSupNonarchAddGroupSeminorm {E : Type u_4} [AddGroup E] : SemilatticeSup (NonarchAddGroupSeminorm E)

theorem NonarchAddGroupSeminorm.add_bddBelow_range_add {E : Type u_4} [AddCommGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} {x : E} : BddBelow (Set.range fun y => ↑p y + ↑q (x - y))

instance GroupSeminorm.toOne {E : Type u_4} [Group E] [DecidableEq E] : One (GroupSeminorm E)

@[simp]

theorem GroupSeminorm.apply_one {E : Type u_4} [Group E] [DecidableEq E] (x : E) : ↑1 x = if x = 1 then 0 else 1

instance GroupSeminorm.instSMulGroupSeminorm {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] : SMul R (GroupSeminorm E)

Any action on ℝ which factors through ℝ≥0 applies to an AddGroupSeminorm.

instance GroupSeminorm.instIsScalarTowerGroupSeminormInstSMulGroupSeminormInstSMulGroupSeminorm {R : Type u_2} {R' : Type u_3} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (GroupSeminorm E)

@[simp]

theorem GroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) : ↑(r • p) = r • ↑p

@[simp]

theorem GroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) (x : E) : ↑(r • p) x = r • ↑p x

theorem GroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) (q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

instance NonarchAddGroupSeminorm.instOneNonarchAddGroupSeminorm {E : Type u_4} [AddGroup E] [DecidableEq E] : One (NonarchAddGroupSeminorm E)

@[simp]

theorem NonarchAddGroupSeminorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) : ↑1 x = if x = 0 then 0 else 1

instance NonarchAddGroupSeminorm.instSMulNonarchAddGroupSeminorm {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] : SMul R (NonarchAddGroupSeminorm E)

Any action on ℝ which factors through ℝ≥0 applies to a NonarchAddGroupSeminorm.

instance NonarchAddGroupSeminorm.instIsScalarTowerNonarchAddGroupSeminormInstSMulNonarchAddGroupSeminormInstSMulNonarchAddGroupSeminorm {R : Type u_2} {R' : Type u_3} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (NonarchAddGroupSeminorm E)

@[simp]

theorem NonarchAddGroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) : ↑(r • p) = r • ↑p

@[simp]

theorem NonarchAddGroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) (x : E) : ↑(r • p) x = r • ↑p x

theorem NonarchAddGroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) (q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

Norms

instance AddGroupNorm.addGroupNormClass {E : Type u_4} [AddGroup E] : AddGroupNormClass (AddGroupNorm E) E ℝ

theorem AddGroupNorm.addGroupNormClass.proof_3 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) : AddGroupSeminorm.toFun f.toAddGroupSeminorm 0 = 0

theorem AddGroupNorm.addGroupNormClass.proof_2 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) (x : E) (y : E) : AddGroupSeminorm.toFun f.toAddGroupSeminorm (x + y) ≤ AddGroupSeminorm.toFun f.toAddGroupSeminorm x + AddGroupSeminorm.toFun f.toAddGroupSeminorm y

theorem AddGroupNorm.addGroupNormClass.proof_4 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) (x : E) : AddGroupSeminorm.toFun f.toAddGroupSeminorm (-x) = AddGroupSeminorm.toFun f.toAddGroupSeminorm x

theorem AddGroupNorm.addGroupNormClass.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) (g : AddGroupNorm E) (h : (fun f => f.toFun) f = (fun f => f.toFun) g) : f = g

instance GroupNorm.groupNormClass {E : Type u_4} [Group E] : GroupNormClass (GroupNorm E) E ℝ

instance AddGroupNorm.instCoeFunAddGroupNormForAllReal {E : Type u_4} [AddGroup E] : CoeFun (AddGroupNorm E) fun x => E → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

instance GroupNorm.instCoeFunGroupNormForAllReal {E : Type u_4} [Group E] : CoeFun (GroupNorm E) fun x => E → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

@[simp]

theorem AddGroupNorm.toAddGroupSeminorm_eq_coe {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} : ↑p.toAddGroupSeminorm = ↑p

@[simp]

theorem GroupNorm.toGroupSeminorm_eq_coe {E : Type u_4} [Group E] {p : GroupNorm E} : ↑p.toGroupSeminorm = ↑p

theorem AddGroupNorm.ext {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : (∀ (x : E), ↑p x = ↑q x) → p = q

theorem GroupNorm.ext {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : (∀ (x : E), ↑p x = ↑q x) → p = q

theorem AddGroupNorm.instPartialOrderAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun f => ↑f

instance AddGroupNorm.instPartialOrderAddGroupNorm {E : Type u_4} [AddGroup E] : PartialOrder (AddGroupNorm E)

instance GroupNorm.instPartialOrderGroupNorm {E : Type u_4} [Group E] : PartialOrder (GroupNorm E)

theorem AddGroupNorm.le_def {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : p ≤ q ↔ ↑p ≤ ↑q

theorem GroupNorm.le_def {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : p ≤ q ↔ ↑p ≤ ↑q

theorem AddGroupNorm.lt_def {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : p < q ↔ ↑p < ↑q

theorem GroupNorm.lt_def {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : p < q ↔ ↑p < ↑q

@[simp]

theorem AddGroupNorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : ↑p ≤ ↑q ↔ p ≤ q

@[simp]

theorem GroupNorm.coe_le_coe {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : ↑p ≤ ↑q ↔ p ≤ q

@[simp]

theorem AddGroupNorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : ↑p < ↑q ↔ p < q

@[simp]

theorem GroupNorm.coe_lt_coe {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : ↑p < ↑q ↔ p < q

instance AddGroupNorm.instAddAddGroupNorm {E : Type u_4} [AddGroup E] : Add (AddGroupNorm E)

theorem AddGroupNorm.instAddAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (_x : E) (hx : AddGroupSeminorm.toFun { toFun := (p.toAddGroupSeminorm + q.toAddGroupSeminorm).toFun, map_zero' := (_ : AddGroupSeminorm.toFun (p.toAddGroupSeminorm + q.toAddGroupSeminorm) 0 = 0), add_le' := (_ : ∀ (r s : E), AddGroupSeminorm.toFun (p.toAddGroupSeminorm + q.toAddGroupSeminorm) (r + s) ≤ AddGroupSeminorm.toFun (p.toAddGroupSeminorm + q.toAddGroupSeminorm) r + AddGroupSeminorm.toFun (p.toAddGroupSeminorm + q.toAddGroupSeminorm) s), neg' := (_ : ∀ (r : E), AddGroupSeminorm.toFun (p.toAddGroupSeminorm + q.toAddGroupSeminorm) (-r) = AddGroupSeminorm.toFun (p.toAddGroupSeminorm + q.toAddGroupSeminorm) r) } _x = 0) : _x = 0

instance GroupNorm.instAddGroupNorm {E : Type u_4} [Group E] : Add (GroupNorm E)

@[simp]

theorem AddGroupNorm.coe_add {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) : ↑(p + q) = ↑p + ↑q

@[simp]

theorem GroupNorm.coe_add {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) : ↑(p + q) = ↑p + ↑q

@[simp]

theorem AddGroupNorm.add_apply {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (x : E) : ↑(p + q) x = ↑p x + ↑q x

@[simp]

theorem GroupNorm.add_apply {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) (x : E) : ↑(p + q) x = ↑p x + ↑q x

instance AddGroupNorm.instSupAddGroupNorm {E : Type u_4} [AddGroup E] : Sup (AddGroupNorm E)

theorem AddGroupNorm.instSupAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (_x : E) (hx : AddGroupSeminorm.toFun { toFun := (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm).toFun, map_zero' := (_ : AddGroupSeminorm.toFun (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm) 0 = 0), add_le' := (_ : ∀ (r s : E), AddGroupSeminorm.toFun (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm) (r + s) ≤ AddGroupSeminorm.toFun (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm) r + AddGroupSeminorm.toFun (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm) s), neg' := (_ : ∀ (r : E), AddGroupSeminorm.toFun (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm) (-r) = AddGroupSeminorm.toFun (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm) r) } _x = 0) : _x = 0

instance GroupNorm.instSupGroupNorm {E : Type u_4} [Group E] : Sup (GroupNorm E)

@[simp]

theorem AddGroupNorm.coe_sup {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) : ↑(p ⊔ q) = ↑p ⊔ ↑q

@[simp]

theorem GroupNorm.coe_sup {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) : ↑(p ⊔ q) = ↑p ⊔ ↑q

@[simp]

theorem AddGroupNorm.sup_apply {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (x : E) : ↑(p ⊔ q) x = ↑p x ⊔ ↑q x

@[simp]

theorem GroupNorm.sup_apply {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) (x : E) : ↑(p ⊔ q) x = ↑p x ⊔ ↑q x

theorem AddGroupNorm.instSemilatticeSupAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun f => ↑f

instance AddGroupNorm.instSemilatticeSupAddGroupNorm {E : Type u_4} [AddGroup E] : SemilatticeSup (AddGroupNorm E)

instance GroupNorm.instSemilatticeSupGroupNorm {E : Type u_4} [Group E] : SemilatticeSup (GroupNorm E)

instance AddGroupNorm.instOneAddGroupNorm {E : Type u_4} [AddGroup E] [DecidableEq E] : One (AddGroupNorm E)

@[simp]

theorem AddGroupNorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) : ↑1 x = if x = 0 then 0 else 1

instance AddGroupNorm.instInhabitedAddGroupNorm {E : Type u_4} [AddGroup E] [DecidableEq E] : Inhabited (AddGroupNorm E)

instance AddGroupNorm.toOne {E : Type u_4} [AddGroup E] [DecidableEq E] : One (AddGroupNorm E)

instance GroupNorm.toOne {E : Type u_4} [Group E] [DecidableEq E] : One (GroupNorm E)

@[simp]

theorem GroupNorm.apply_one {E : Type u_4} [Group E] [DecidableEq E] (x : E) : ↑1 x = if x = 1 then 0 else 1

instance GroupNorm.instInhabitedGroupNorm {E : Type u_4} [Group E] [DecidableEq E] : Inhabited (GroupNorm E)

instance NonarchAddGroupNorm.nonarchAddGroupNormClass {E : Type u_4} [AddGroup E] : NonarchAddGroupNormClass (NonarchAddGroupNorm E) E

noncomputable instance NonarchAddGroupNorm.instCoeFunNonarchAddGroupNormForAllReal {E : Type u_4} [AddGroup E] : CoeFun (NonarchAddGroupNorm E) fun x => E → ℝ

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

@[simp]

theorem NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} : ↑p.toNonarchAddGroupSeminorm = ↑p

theorem NonarchAddGroupNorm.ext {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : (∀ (x : E), ↑p x = ↑q x) → p = q

noncomputable instance NonarchAddGroupNorm.instPartialOrderNonarchAddGroupNorm {E : Type u_4} [AddGroup E] : PartialOrder (NonarchAddGroupNorm E)

theorem NonarchAddGroupNorm.le_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : p ≤ q ↔ ↑p ≤ ↑q

theorem NonarchAddGroupNorm.lt_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : p < q ↔ ↑p < ↑q

@[simp]

theorem NonarchAddGroupNorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : ↑p ≤ ↑q ↔ p ≤ q

@[simp]

theorem NonarchAddGroupNorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : ↑p < ↑q ↔ p < q

instance NonarchAddGroupNorm.instSupNonarchAddGroupNorm {E : Type u_4} [AddGroup E] : Sup (NonarchAddGroupNorm E)

@[simp]

theorem NonarchAddGroupNorm.coe_sup {E : Type u_4} [AddGroup E] (p : NonarchAddGroupNorm E) (q : NonarchAddGroupNorm E) : ↑(p ⊔ q) = ↑p ⊔ ↑q

@[simp]

theorem NonarchAddGroupNorm.sup_apply {E : Type u_4} [AddGroup E] (p : NonarchAddGroupNorm E) (q : NonarchAddGroupNorm E) (x : E) : ↑(p ⊔ q) x = ↑p x ⊔ ↑q x

noncomputable instance NonarchAddGroupNorm.instSemilatticeSupNonarchAddGroupNorm {E : Type u_4} [AddGroup E] : SemilatticeSup (NonarchAddGroupNorm E)

instance NonarchAddGroupNorm.instOneNonarchAddGroupNorm {E : Type u_4} [AddGroup E] [DecidableEq E] : One (NonarchAddGroupNorm E)

@[simp]

theorem NonarchAddGroupNorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) : ↑1 x = if x = 0 then 0 else 1

instance NonarchAddGroupNorm.instInhabitedNonarchAddGroupNorm {E : Type u_4} [AddGroup E] [DecidableEq E] : Inhabited (NonarchAddGroupNorm E)