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

source

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

Type u_7

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.

toFun : G → ℝ
The bare function of an AddGroupSeminorm.
map_zero' : self.toFun 0 = 0
The image of zero is zero.
add_le' : ∀ (r s : G), self.toFun (r + s) ≤ self.toFun r + self.toFun s
The seminorm is subadditive.
neg' : ∀ (r : G), self.toFun (-r) = self.toFun r
The seminorm is invariant under negation.

Instances For

source

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

Type u_7

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.

toFun : G → ℝ
The bare function of a GroupSeminorm.
map_one' : self.toFun 1 = 0
The image of one is zero.
mul_le' : ∀ (x y : G), self.toFun (x * y) ≤ self.toFun x + self.toFun y
The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.
inv' : ∀ (x : G), self.toFun x⁻¹ = self.toFun x
The seminorm is invariant under inversion.

Instances For

source

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

Type u_7

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.

toFun : G → ℝ
map_zero' : self.toFun 0 = 0
add_le_max' : ∀ (r s : G), self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.
neg' : ∀ (r : G), self.toFun (-r) = self.toFun r
The seminorm is invariant under negation.

Instances For

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.

source

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

Type u_7

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.

toFun : G → ℝ
map_zero' : self.toFun 0 = 0
add_le' : ∀ (r s : G), self.toFun (r + s) ≤ self.toFun r + self.toFun s
neg' : ∀ (r : G), self.toFun (-r) = self.toFun r
eq_zero_of_map_eq_zero' : ∀ (x : G), self.toFun x = 0 → x = 0
If the image under the seminorm is zero, then the argument is zero.

Instances For

source

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

Type u_7

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.

toFun : G → ℝ
map_one' : self.toFun 1 = 0
mul_le' : ∀ (x y : G), self.toFun (x * y) ≤ self.toFun x + self.toFun y
inv' : ∀ (x : G), self.toFun x⁻¹ = self.toFun x
eq_one_of_map_eq_zero' : ∀ (x : G), self.toFun x = 0 → x = 1
If the image under the norm is zero, then the argument is one.

Instances For

source

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

Type u_7

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.

toFun : G → ℝ
map_zero' : self.toFun 0 = 0
add_le_max' : ∀ (r s : G), self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
neg' : ∀ (r : G), self.toFun (-r) = self.toFun r
eq_zero_of_map_eq_zero' : ∀ (x : G), self.toFun x = 0 → x = 0
If the image under the norm is zero, then the argument is zero.

Instances For

source

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

Prop

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

You should extend this class when you extend NonarchAddGroupSeminorm.

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.

Instances

NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass

source

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

Prop

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

You should extend this class when you extend NonarchAddGroupNorm.

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.

Instances

NonarchAddGroupNorm.nonarchAddGroupNormClass

source

theorem map_sub_le_max {E : Type u_4} {F : Type u_5} [AddGroup E] [FunLike F E ℝ] [NonarchAddGroupSeminormClass F E] (f : F) (x : E) (y : E) :

f (x - y) ≤ max (f x) (f y)

source

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

AddGroupSeminormClass F E ℝ

Equations

⋯ = ⋯

source

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

AddGroupNormClass F E ℝ

Equations

⋯ = ⋯

Seminorms #

source

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

f = g

source

instance AddGroupSeminorm.funLike {E : Type u_4} [AddGroup E] :

FunLike (AddGroupSeminorm E) E ℝ

Equations

AddGroupSeminorm.funLike = { coe := fun (f : AddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

source

instance GroupSeminorm.funLike {E : Type u_4} [Group E] :

FunLike (GroupSeminorm E) E ℝ

Equations

GroupSeminorm.funLike = { coe := fun (f : GroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

source

instance AddGroupSeminorm.addGroupSeminormClass {E : Type u_4} [AddGroup E] :

AddGroupSeminormClass (AddGroupSeminorm E) E ℝ

Equations

⋯ = ⋯

source

instance GroupSeminorm.groupSeminormClass {E : Type u_4} [Group E] :

GroupSeminormClass (GroupSeminorm E) E ℝ

Equations

⋯ = ⋯

source

instance AddGroupSeminorm.instCoeFunAddGroupSeminormForAllReal {E : Type u_4} [AddGroup E] :

CoeFun (AddGroupSeminorm E) fun (x : AddGroupSeminorm E) => E → ℝ

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

Equations

AddGroupSeminorm.instCoeFunAddGroupSeminormForAllReal = { coe := DFunLike.coe }

source

instance GroupSeminorm.instCoeFunGroupSeminormForAllReal {E : Type u_4} [Group E] :

CoeFun (GroupSeminorm E) fun (x : GroupSeminorm E) => E → ℝ

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

Equations

GroupSeminorm.instCoeFunGroupSeminormForAllReal = { coe := DFunLike.coe }

source

@[simp]

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

p.toFun = ⇑p

source

@[simp]

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

p.toFun = ⇑p

source

theorem AddGroupSeminorm.ext {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} :

(∀ (x : E), p x = q x) → p = q

source

theorem GroupSeminorm.ext {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} :

(∀ (x : E), p x = q x) → p = q

source

theorem AddGroupSeminorm.instPartialOrderAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] :

Function.Injective fun (f : AddGroupSeminorm E) => ⇑f

source

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

PartialOrder (AddGroupSeminorm E)

Equations

AddGroupSeminorm.instPartialOrderAddGroupSeminorm = PartialOrder.lift (fun (f : AddGroupSeminorm E) => ⇑f) ⋯

source

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

PartialOrder (GroupSeminorm E)

Equations

GroupSeminorm.instPartialOrderGroupSeminorm = PartialOrder.lift (fun (f : GroupSeminorm E) => ⇑f) ⋯

source

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

p ≤ q ↔ ⇑p ≤ ⇑q

source

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

p ≤ q ↔ ⇑p ≤ ⇑q

source

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

p < q ↔ ⇑p < ⇑q

source

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

p < q ↔ ⇑p < ⇑q

source

@[simp]

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

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

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

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

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

⇑p < ⇑q ↔ p < q

source

@[simp]

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

⇑p < ⇑q ↔ p < q

source

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

Zero (AddGroupSeminorm E)

Equations

AddGroupSeminorm.instZeroAddGroupSeminorm = { zero := { toFun := 0, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] :

0 0 = 0

source

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_2 {E : Type u_1} [AddGroup E] :

∀ (x x_1 : E), 0 (x + x_1) ≤ 0 + 0 (x + x_1)

source

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_3 {E : Type u_1} [AddGroup E] :

∀ (x : E), 0 (-x) = 0 (-x)

source

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

Zero (GroupSeminorm E)

Equations

GroupSeminorm.instZeroGroupSeminorm = { zero := { toFun := 0, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source

@[simp]

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

⇑0 = 0

source

@[simp]

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

⇑0 = 0

source

@[simp]

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

0 x = 0

source

@[simp]

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

0 x = 0

source

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

Inhabited (AddGroupSeminorm E)

Equations

AddGroupSeminorm.instInhabitedAddGroupSeminorm = { default := 0 }

source

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

Inhabited (GroupSeminorm E)

Equations

GroupSeminorm.instInhabitedGroupSeminorm = { default := 0 }

source

theorem AddGroupSeminorm.instAddAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) :

(fun (x : E) => p x + q x) 0 = 0

source

theorem AddGroupSeminorm.instAddAddGroupSeminorm.proof_3 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) :

(fun (x : E) => p x + q x) (-x) = (fun (x : E) => p x + q x) x

source

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 : E) => p x + q x) x + (fun (x : E) => p x + q x) x_1

source

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

Add (AddGroupSeminorm E)

Equations

AddGroupSeminorm.instAddAddGroupSeminorm = { add := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source

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

Add (GroupSeminorm E)

Equations

GroupSeminorm.instAddGroupSeminorm = { add := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source

@[simp]

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

⇑(p + q) = ⇑p + ⇑q

source

@[simp]

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

⇑(p + q) = ⇑p + ⇑q

source

@[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

source

@[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

source

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

source

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

(⇑p ⊔ ⇑q) 0 = 0

source

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

source

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

Sup (AddGroupSeminorm E)

Equations

AddGroupSeminorm.instSupAddGroupSeminorm = { sup := fun (p q : AddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source

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

Sup (GroupSeminorm E)

Equations

GroupSeminorm.instSupGroupSeminorm = { sup := fun (p q : GroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source

@[simp]

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

⇑(p ⊔ q) = ⇑p ⊔ ⇑q

source

@[simp]

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

⇑(p ⊔ q) = ⇑p ⊔ ⇑q

source

@[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

source

@[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

source

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

SemilatticeSup (AddGroupSeminorm E)

Equations

AddGroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupSeminorm E) => ⇑f) ⋯ ⋯

source

theorem AddGroupSeminorm.semilatticeSup.proof_1 {E : Type u_1} [AddGroup E] :

Function.Injective fun (f : AddGroupSeminorm E) => ⇑f

source

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

SemilatticeSup (GroupSeminorm E)

Equations

GroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupSeminorm E) => ⇑f) ⋯ ⋯

source

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.

Equations

AddGroupSeminorm.comp p f = { toFun := fun (x : F) => p (f x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }

source

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 : F) => p (f x)) (-x) = (fun (x : F) => p (f x)) x

source

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 : F) => p (f x)) x + (fun (x : F) => p (f x)) x_1

source

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 : F) => p (f x)) 0 = 0

source

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.

Equations

GroupSeminorm.comp p f = { toFun := fun (x : F) => p (f x), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }

source

@[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

source

@[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

source

@[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)

source

@[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)

source

@[simp]

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

AddGroupSeminorm.comp p (AddMonoidHom.id E) = p

source

@[simp]

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

GroupSeminorm.comp p (MonoidHom.id E) = p

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 : E) => p y + q (x - y))

source

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 : E) => p y + q (x / y))

source

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

Inf (AddGroupSeminorm E)

Equations

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

source

theorem AddGroupSeminorm.instInfAddGroupSeminormToAddGroup.proof_2 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) (y : E) :

(fun (x : E) => ⨅ (y : E), p y + q (x - y)) (x + y) ≤ (⨅ (y : E), p y + q (x - y)) + ⨅ (y_1 : E), p y_1 + q (y - y_1)

source

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

source

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 : E) => ⨅ (y : E), p y + q (x - y)) x

source

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

Inf (GroupSeminorm E)

Equations

GroupSeminorm.instInfGroupSeminormToGroup = { inf := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x / y), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source

@[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)

source

@[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)

source

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

Lattice (AddGroupSeminorm E)

Equations

AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup = let __src := AddGroupSeminorm.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯

source

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_3 {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 : AddGroupSeminorm E) => ⇑f) a x ≤ ⨅ (y : E), b y + c (x - y)

source

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_2 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) :

⨅ (y : E), p y + q (x - y) ≤ (fun (f : AddGroupSeminorm E) => ⇑f) q x

source

theorem AddGroupSeminorm.instLatticeAddGroupSeminormToAddGroup.proof_1 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) :

⨅ (y : E), p y + q (x - y) ≤ (fun (f : AddGroupSeminorm E) => ⇑f) p x

source

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

Lattice (GroupSeminorm E)

Equations

GroupSeminorm.instLatticeGroupSeminormToGroup = let __src := GroupSeminorm.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯

source

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

One (AddGroupSeminorm E)

Equations

AddGroupSeminorm.toOne = { one := { toFun := fun (x : E) => if x = 0 then 0 else 1, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source

@[simp]

theorem AddGroupSeminorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) :

1 x = if x = 0 then 0 else 1

source

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.

Equations

AddGroupSeminorm.toSMul = { smul := fun (r : R) (p : AddGroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source

@[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

source

@[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

source

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)

Equations

⋯ = ⋯

source

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

source

instance NonarchAddGroupSeminorm.funLike {E : Type u_4} [AddGroup E] :

FunLike (NonarchAddGroupSeminorm E) E ℝ

Equations

NonarchAddGroupSeminorm.funLike = { coe := fun (f : NonarchAddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

source

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

NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E

Equations

⋯ = ⋯

source

instance NonarchAddGroupSeminorm.instCoeFunNonarchAddGroupSeminormForAllReal {E : Type u_4} [AddGroup E] :

CoeFun (NonarchAddGroupSeminorm E) fun (x : NonarchAddGroupSeminorm E) => E → ℝ

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

Equations

NonarchAddGroupSeminorm.instCoeFunNonarchAddGroupSeminormForAllReal = { coe := DFunLike.coe }

source

@[simp]

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

⇑p.toZeroHom = ⇑p

source

theorem NonarchAddGroupSeminorm.ext {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} :

(∀ (x : E), p x = q x) → p = q

source

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

PartialOrder (NonarchAddGroupSeminorm E)

Equations

NonarchAddGroupSeminorm.instPartialOrderNonarchAddGroupSeminorm = PartialOrder.lift (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯

source

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

p ≤ q ↔ ⇑p ≤ ⇑q

source

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

p < q ↔ ⇑p < ⇑q

source

@[simp]

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

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

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

⇑p < ⇑q ↔ p < q

source

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

Zero (NonarchAddGroupSeminorm E)

Equations

NonarchAddGroupSeminorm.instZeroNonarchAddGroupSeminorm = { zero := { toZeroHom := { toFun := 0, map_zero' := ⋯ }, add_le_max' := ⋯, neg' := ⋯ } }

source

@[simp]

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

⇑0 = 0

source

@[simp]

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

0 x = 0

source

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

Inhabited (NonarchAddGroupSeminorm E)

Equations

NonarchAddGroupSeminorm.instInhabitedNonarchAddGroupSeminorm = { default := 0 }

source

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

Sup (NonarchAddGroupSeminorm E)

Equations

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

source

@[simp]

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

⇑(p ⊔ q) = ⇑p ⊔ ⇑q

source

@[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

source

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

SemilatticeSup (NonarchAddGroupSeminorm E)

Equations

NonarchAddGroupSeminorm.instSemilatticeSupNonarchAddGroupSeminorm = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯ ⋯

source

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 : E) => p y + q (x - y))

source

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

One (GroupSeminorm E)

Equations

GroupSeminorm.toOne = { one := { toFun := fun (x : E) => if x = 1 then 0 else 1, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source

@[simp]

theorem GroupSeminorm.apply_one {E : Type u_4} [Group E] [DecidableEq E] (x : E) :

1 x = if x = 1 then 0 else 1

source

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.

Equations

GroupSeminorm.instSMulGroupSeminorm = { smul := fun (r : R) (p : GroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source

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)

Equations

⋯ = ⋯

source

@[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

source

@[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

source

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

source

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

One (NonarchAddGroupSeminorm E)

Equations

NonarchAddGroupSeminorm.instOneNonarchAddGroupSeminorm = { one := { toZeroHom := { toFun := fun (x : E) => if x = 0 then 0 else 1, map_zero' := ⋯ }, add_le_max' := ⋯, neg' := ⋯ } }

source

@[simp]

theorem NonarchAddGroupSeminorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) :

1 x = if x = 0 then 0 else 1

source

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.

Equations

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

source

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)

Equations

⋯ = ⋯

source

@[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

source

@[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

source

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 #

source

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

f = g

source

instance AddGroupNorm.funLike {E : Type u_4} [AddGroup E] :

FunLike (AddGroupNorm E) E ℝ

Equations

AddGroupNorm.funLike = { coe := fun (f : AddGroupNorm E) => f.toFun, coe_injective' := ⋯ }

source

instance GroupNorm.funLike {E : Type u_4} [Group E] :

FunLike (GroupNorm E) E ℝ

Equations

GroupNorm.funLike = { coe := fun (f : GroupNorm E) => f.toFun, coe_injective' := ⋯ }

source

instance AddGroupNorm.addGroupNormClass {E : Type u_4} [AddGroup E] :

AddGroupNormClass (AddGroupNorm E) E ℝ

Equations

⋯ = ⋯

source

instance GroupNorm.groupNormClass {E : Type u_4} [Group E] :

GroupNormClass (GroupNorm E) E ℝ

Equations

⋯ = ⋯

source

instance AddGroupNorm.instCoeFunAddGroupNormForAllReal {E : Type u_4} [AddGroup E] :

CoeFun (AddGroupNorm E) fun (x : AddGroupNorm E) => E → ℝ

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

Equations

AddGroupNorm.instCoeFunAddGroupNormForAllReal = DFunLike.hasCoeToFun

source

instance GroupNorm.instCoeFunGroupNormForAllReal {E : Type u_4} [Group E] :

CoeFun (GroupNorm E) fun (x : GroupNorm E) => E → ℝ

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

Equations

GroupNorm.instCoeFunGroupNormForAllReal = DFunLike.hasCoeToFun

source

@[simp]

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

⇑p.toAddGroupSeminorm = ⇑p

source

@[simp]

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

⇑p.toGroupSeminorm = ⇑p

source

theorem AddGroupNorm.ext {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} :

(∀ (x : E), p x = q x) → p = q

source

theorem GroupNorm.ext {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} :

(∀ (x : E), p x = q x) → p = q

source

theorem AddGroupNorm.instPartialOrderAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] :

Function.Injective fun (f : AddGroupNorm E) => ⇑f

source

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

PartialOrder (AddGroupNorm E)

Equations

AddGroupNorm.instPartialOrderAddGroupNorm = PartialOrder.lift (fun (f : AddGroupNorm E) => ⇑f) ⋯

source

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

PartialOrder (GroupNorm E)

Equations

GroupNorm.instPartialOrderGroupNorm = PartialOrder.lift (fun (f : GroupNorm E) => ⇑f) ⋯

source

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

p ≤ q ↔ ⇑p ≤ ⇑q

source

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

p ≤ q ↔ ⇑p ≤ ⇑q

source

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

p < q ↔ ⇑p < ⇑q

source

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

p < q ↔ ⇑p < ⇑q

source

@[simp]

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

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

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

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

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

⇑p < ⇑q ↔ p < q

source

@[simp]

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

⇑p < ⇑q ↔ p < q

source

theorem AddGroupNorm.instAddAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (_x : E) (hx : (p.toAddGroupSeminorm + q.toAddGroupSeminorm).toFun _x = 0) :

_x = 0

source

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

Add (AddGroupNorm E)

Equations

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

source

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

Add (GroupNorm E)

Equations

GroupNorm.instAddGroupNorm = { add := fun (p q : GroupNorm E) => let __src := p.toGroupSeminorm + q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

source

@[simp]

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

⇑(p + q) = ⇑p + ⇑q

source

@[simp]

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

⇑(p + q) = ⇑p + ⇑q

source

@[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

source

@[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

source

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

Sup (AddGroupNorm E)

Equations

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

source

theorem AddGroupNorm.instSupAddGroupNorm.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (_x : E) (hx : (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm).toFun _x = 0) :

_x = 0

source

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

Sup (GroupNorm E)

Equations

GroupNorm.instSupGroupNorm = { sup := fun (p q : GroupNorm E) => let __src := p.toGroupSeminorm ⊔ q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }