analysis.normed.group.seminorm

@[nolint]

def add_group_seminorm.to_zero_hom {G : Type u_7} [add_group G] (self : add_group_seminorm G) :

structure add_group_seminorm (G : Type u_7) [add_group G] :

to_fun : G → ℝ
map_zero' : self.to_fun 0 = 0
add_le' : ∀ (r s : G), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
neg' : ∀ (r : G), self.to_fun (-r) = self.to_fun r

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.

Instances for add_group_seminorm

source

structure group_seminorm (G : Type u_7) [group G] :

Type u_7

to_fun : G → ℝ
map_one' : self.to_fun 1 = 0
mul_le' : ∀ (x y : G), self.to_fun (x * y) ≤ self.to_fun x + self.to_fun y
inv' : ∀ (x : G), self.to_fun x⁻¹ = self.to_fun x

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.

Instances for group_seminorm

source

@[nolint]

def nonarch_add_group_seminorm.to_zero_hom {G : Type u_7} [add_group G] (self : nonarch_add_group_seminorm G) :

zero_hom G ℝ

source

structure nonarch_add_group_seminorm (G : Type u_7) [add_group G] :

Type u_7

to_fun : G → ℝ
map_zero' : self.to_fun 0 = 0
add_le_max' : ∀ (r s : G), self.to_fun (r + s) ≤ linear_order.max (self.to_fun r) (self.to_fun s)
neg' : ∀ (r : G), self.to_fun (-r) = self.to_fun r

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.

Instances for nonarch_add_group_seminorm

source

structure add_group_norm (G : Type u_7) [add_group G] :

Type u_7

to_fun : G → ℝ
map_zero' : self.to_fun 0 = 0
add_le' : ∀ (r s : G), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
neg' : ∀ (r : G), self.to_fun (-r) = self.to_fun r
eq_zero_of_map_eq_zero' : ∀ (x : G), self.to_fun x = 0 → x = 0

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.

Instances for add_group_norm

source

@[nolint]

def add_group_norm.to_add_group_seminorm {G : Type u_7} [add_group G] (self : add_group_norm G) :

add_group_seminorm G

source

@[nolint]

def group_norm.to_group_seminorm {G : Type u_7} [group G] (self : group_norm G) :

group_seminorm G

source

structure group_norm (G : Type u_7) [group G] :

Type u_7

to_fun : G → ℝ
map_one' : self.to_fun 1 = 0
mul_le' : ∀ (x y : G), self.to_fun (x * y) ≤ self.to_fun x + self.to_fun y
inv' : ∀ (x : G), self.to_fun x⁻¹ = self.to_fun x
eq_one_of_map_eq_zero' : ∀ (x : G), self.to_fun x = 0 → x = 1

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.

Instances for group_norm

source

@[nolint]

def nonarch_add_group_norm.to_nonarch_add_group_seminorm {G : Type u_7} [add_group G] (self : nonarch_add_group_norm G) :

nonarch_add_group_seminorm G

source

structure nonarch_add_group_norm (G : Type u_7) [add_group G] :

Type u_7

to_fun : G → ℝ
map_zero' : self.to_fun 0 = 0
add_le_max' : ∀ (r s : G), self.to_fun (r + s) ≤ linear_order.max (self.to_fun r) (self.to_fun s)
neg' : ∀ (r : G), self.to_fun (-r) = self.to_fun r
eq_zero_of_map_eq_zero' : ∀ (x : G), self.to_fun x = 0 → x = 0

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.

Instances for nonarch_add_group_norm

nonarch_add_group_norm.has_sizeof_inst
nonarch_add_group_norm.nonarch_add_group_norm_class
nonarch_add_group_norm.has_coe_to_fun
nonarch_add_group_norm.partial_order
nonarch_add_group_norm.has_sup
nonarch_add_group_norm.semilattice_sup
nonarch_add_group_norm.has_one
nonarch_add_group_norm.inhabited

source

@[class]

structure nonarch_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] :

Type (max u_7 u_8)

coe : F → Π (a : α), (λ (_x : α), ℝ) a
coe_injective' : function.injective nonarch_add_group_seminorm_class.coe
map_add_le_max : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ linear_order.max (⇑f a) (⇑f b)
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map' : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a

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

You should extend this class when you extend nonarch_add_group_seminorm.

Instances of this typeclass

Instances of other typeclasses for nonarch_add_group_seminorm_class

nonarch_add_group_seminorm_class.has_sizeof_inst

source

@[instance]

def nonarch_add_group_seminorm_class.to_nonarchimedean_hom_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] [self : nonarch_add_group_seminorm_class F α] :

nonarchimedean_hom_class F α ℝ

source

@[class]

structure nonarch_add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] :

Type (max u_7 u_8)

coe : F → Π (a : α), (λ (_x : α), ℝ) a
coe_injective' : function.injective nonarch_add_group_norm_class.coe
map_add_le_max : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ linear_order.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

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

You should extend this class when you extend nonarch_add_group_norm.

Instances of this typeclass

nonarch_add_group_norm.nonarch_add_group_norm_class

Instances of other typeclasses for nonarch_add_group_norm_class

nonarch_add_group_norm_class.has_sizeof_inst

source

@[instance]

def nonarch_add_group_norm_class.to_nonarch_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] [self : nonarch_add_group_norm_class F α] :

nonarch_add_group_seminorm_class F α

source

theorem map_sub_le_max {E : Type u_4} {F : Type u_5} [add_group E] [nonarch_add_group_seminorm_class F E] (f : F) (x y : E) :

⇑f (x - y) ≤ linear_order.max (⇑f x) (⇑f y)

source

@[protected, instance]

def nonarch_add_group_seminorm_class.to_add_group_seminorm_class {E : Type u_4} {F : Type u_5} [add_group E] [nonarch_add_group_seminorm_class F E] :

add_group_seminorm_class F E ℝ

Equations

nonarch_add_group_seminorm_class.to_add_group_seminorm_class = {coe := nonarch_add_group_seminorm_class.coe _inst_2, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _}

source

@[protected, instance]

def nonarch_add_group_norm_class.to_add_group_norm_class {E : Type u_4} {F : Type u_5} [add_group E] [nonarch_add_group_norm_class F E] :

add_group_norm_class F E ℝ

Equations

nonarch_add_group_norm_class.to_add_group_norm_class = {coe := nonarch_add_group_norm_class.coe _inst_2, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, eq_zero_of_map_eq_zero := _}

source

@[protected, instance]

def group_seminorm.group_seminorm_class {E : Type u_4} [group E] :

group_seminorm_class (group_seminorm E) E ℝ

Equations

group_seminorm.group_seminorm_class = {coe := λ (f : group_seminorm E), f.to_fun, coe_injective' := _, map_mul_le_add := _, map_one_eq_zero := _, map_inv_eq_map := _}

source

@[protected, instance]

def add_group_seminorm.add_group_seminorm_class {E : Type u_4} [add_group E] :

add_group_seminorm_class (add_group_seminorm E) E ℝ

Equations

add_group_seminorm.add_group_seminorm_class = {coe := λ (f : add_group_seminorm E), f.to_fun, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _}

source

@[protected, instance]

def add_group_seminorm.has_coe_to_fun {E : Type u_4} [add_group E] :

has_coe_to_fun (add_group_seminorm E) (λ (_x : add_group_seminorm E), E → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

add_group_seminorm.has_coe_to_fun = {coe := add_group_seminorm.to_fun _inst_1}

source

@[protected, instance]

def group_seminorm.has_coe_to_fun {E : Type u_4} [group E] :

has_coe_to_fun (group_seminorm E) (λ (_x : group_seminorm E), E → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

group_seminorm.has_coe_to_fun = {coe := group_seminorm.to_fun _inst_1}

source

@[simp]

theorem add_group_seminorm.to_fun_eq_coe {E : Type u_4} [add_group E] {p : add_group_seminorm E} :

p.to_fun = ⇑p

source

@[simp]

theorem group_seminorm.to_fun_eq_coe {E : Type u_4} [group E] {p : group_seminorm E} :

p.to_fun = ⇑p

source

@[ext]

theorem group_seminorm.ext {E : Type u_4} [group E] {p q : group_seminorm E} :

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

source

@[ext]

theorem add_group_seminorm.ext {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :

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

source

@[protected, instance]

def add_group_seminorm.partial_order {E : Type u_4} [add_group E] :

partial_order (add_group_seminorm E)

Equations

add_group_seminorm.partial_order = partial_order.lift coe_fn add_group_seminorm.partial_order._proof_1

source

@[protected, instance]

def group_seminorm.partial_order {E : Type u_4} [group E] :

partial_order (group_seminorm E)

Equations

group_seminorm.partial_order = partial_order.lift coe_fn group_seminorm.partial_order._proof_1

source

theorem group_seminorm.le_def {E : Type u_4} [group E] {p q : group_seminorm E} :

p ≤ q ↔ ⇑p ≤ ⇑q

source

theorem add_group_seminorm.le_def {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :

p ≤ q ↔ ⇑p ≤ ⇑q

source

theorem add_group_seminorm.lt_def {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :

p < q ↔ ⇑p < ⇑q

source

theorem group_seminorm.lt_def {E : Type u_4} [group E] {p q : group_seminorm E} :

p < q ↔ ⇑p < ⇑q

source

@[simp, norm_cast]

theorem group_seminorm.coe_le_coe {E : Type u_4} [group E] {p q : group_seminorm E} :

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

theorem add_group_seminorm.coe_le_coe {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp, norm_cast]

theorem group_seminorm.coe_lt_coe {E : Type u_4} [group E] {p q : group_seminorm E} :

⇑p < ⇑q ↔ p < q

source

@[simp]

theorem add_group_seminorm.coe_lt_coe {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :

⇑p < ⇑q ↔ p < q

source

@[protected, instance]

def add_group_seminorm.has_zero {E : Type u_4} [add_group E] :

has_zero (add_group_seminorm E)

Equations

add_group_seminorm.has_zero = {zero := {to_fun := 0, map_zero' := _, add_le' := _, neg' := _}}

source

@[protected, instance]

def group_seminorm.has_zero {E : Type u_4} [group E] :

has_zero (group_seminorm E)

Equations

group_seminorm.has_zero = {zero := {to_fun := 0, map_one' := _, mul_le' := _, inv' := _}}

source

@[simp]

theorem add_group_seminorm.coe_zero {E : Type u_4} [add_group E] :

⇑0 = 0

source

@[simp, norm_cast]

theorem group_seminorm.coe_zero {E : Type u_4} [group E] :

⇑0 = 0

source

@[simp]

theorem add_group_seminorm.zero_apply {E : Type u_4} [add_group E] (x : E) :

⇑0 x = 0

source

@[simp]

theorem group_seminorm.zero_apply {E : Type u_4} [group E] (x : E) :

⇑0 x = 0

source

@[protected, instance]

def group_seminorm.inhabited {E : Type u_4} [group E] :

inhabited (group_seminorm E)

Equations

group_seminorm.inhabited = {default := 0}

source

@[protected, instance]

def add_group_seminorm.inhabited {E : Type u_4} [add_group E] :

inhabited (add_group_seminorm E)

Equations

add_group_seminorm.inhabited = {default := 0}

source

@[protected, instance]

def group_seminorm.has_add {E : Type u_4} [group E] :

has_add (group_seminorm E)

Equations

group_seminorm.has_add = {add := λ (p q : group_seminorm E), {to_fun := λ (x : E), ⇑p x + ⇑q x, map_one' := _, mul_le' := _, inv' := _}}

source

@[protected, instance]

def add_group_seminorm.has_add {E : Type u_4} [add_group E] :

has_add (add_group_seminorm E)

Equations

add_group_seminorm.has_add = {add := λ (p q : add_group_seminorm E), {to_fun := λ (x : E), ⇑p x + ⇑q x, map_zero' := _, add_le' := _, neg' := _}}

source

@[simp]

theorem add_group_seminorm.coe_add {E : Type u_4} [add_group E] (p q : add_group_seminorm E) :

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

source

@[simp]

theorem group_seminorm.coe_add {E : Type u_4} [group E] (p q : group_seminorm E) :

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

source

@[simp]

theorem add_group_seminorm.add_apply {E : Type u_4} [add_group E] (p q : add_group_seminorm E) (x : E) :

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

source

@[simp]

theorem group_seminorm.add_apply {E : Type u_4} [group E] (p q : group_seminorm E) (x : E) :

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

source

@[protected, instance]

def group_seminorm.has_sup {E : Type u_4} [group E] :

has_sup (group_seminorm E)

Equations

group_seminorm.has_sup = {sup := λ (p q : group_seminorm E), {to_fun := ⇑p ⊔ ⇑q, map_one' := _, mul_le' := _, inv' := _}}

source

@[protected, instance]

def add_group_seminorm.has_sup {E : Type u_4} [add_group E] :

has_sup (add_group_seminorm E)

Equations

add_group_seminorm.has_sup = {sup := λ (p q : add_group_seminorm E), {to_fun := ⇑p ⊔ ⇑q, map_zero' := _, add_le' := _, neg' := _}}

source

@[simp]

theorem add_group_seminorm.coe_sup {E : Type u_4} [add_group E] (p q : add_group_seminorm E) :

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

source

@[simp, norm_cast]

theorem group_seminorm.coe_sup {E : Type u_4} [group E] (p q : group_seminorm E) :

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

source

@[simp]

theorem add_group_seminorm.sup_apply {E : Type u_4} [add_group E] (p q : add_group_seminorm E) (x : E) :

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

source

@[simp]

theorem group_seminorm.sup_apply {E : Type u_4} [group E] (p q : group_seminorm E) (x : E) :

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

source

@[protected, instance]

def group_seminorm.semilattice_sup {E : Type u_4} [group E] :

semilattice_sup (group_seminorm E)

Equations

group_seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn group_seminorm.semilattice_sup._proof_1 group_seminorm.coe_sup

source

@[protected, instance]

def add_group_seminorm.semilattice_sup {E : Type u_4} [add_group E] :

semilattice_sup (add_group_seminorm E)

Equations

add_group_seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn add_group_seminorm.semilattice_sup._proof_1 add_group_seminorm.coe_sup

source

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

add_group_seminorm F

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

Equations

p.comp f = {to_fun := λ (x : F), ⇑p (⇑f x), map_zero' := _, add_le' := _, neg' := _}

source

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

group_seminorm F

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

Equations

p.comp f = {to_fun := λ (x : F), ⇑p (⇑f x), map_one' := _, mul_le' := _, inv' := _}

source

@[simp]

theorem add_group_seminorm.coe_comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) (f : F →+ E) :

⇑(p.comp f) = ⇑p ∘ ⇑f

source

@[simp]

theorem group_seminorm.coe_comp {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) (f : F →* E) :

⇑(p.comp f) = ⇑p ∘ ⇑f

source

@[simp]

theorem add_group_seminorm.comp_apply {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) (f : F →+ E) (x : F) :

⇑(p.comp f) x = ⇑p (⇑f x)

source

@[simp]

theorem group_seminorm.comp_apply {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) (f : F →* E) (x : F) :

⇑(p.comp f) x = ⇑p (⇑f x)

source

@[simp]

theorem add_group_seminorm.comp_id {E : Type u_4} [add_group E] (p : add_group_seminorm E) :

p.comp (add_monoid_hom.id E) = p

source

@[simp]

theorem group_seminorm.comp_id {E : Type u_4} [group E] (p : group_seminorm E) :

p.comp (monoid_hom.id E) = p

source

@[simp]

theorem add_group_seminorm.comp_zero {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) :

p.comp 0 = 0

source

@[simp]

theorem group_seminorm.comp_zero {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) :

p.comp 1 = 0

source

@[simp]

theorem group_seminorm.zero_comp {E : Type u_4} {F : Type u_5} [group E] [group F] (f : F →* E) :

0.comp f = 0

source

@[simp]

theorem add_group_seminorm.zero_comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (f : F →+ E) :

0.comp f = 0

source

theorem group_seminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [group E] [group F] [group G] (p : group_seminorm E) (g : F →* E) (f : G →* F) :

p.comp (g.comp f) = (p.comp g).comp f

source

theorem add_group_seminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [add_group E] [add_group F] [add_group G] (p : add_group_seminorm E) (g : F →+ E) (f : G →+ F) :

p.comp (g.comp f) = (p.comp g).comp f

source

theorem add_group_seminorm.add_comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p q : add_group_seminorm E) (f : F →+ E) :

(p + q).comp f = p.comp f + q.comp f

source

theorem group_seminorm.add_comp {E : Type u_4} {F : Type u_5} [group E] [group F] (p q : group_seminorm E) (f : F →* E) :

(p + q).comp f = p.comp f + q.comp f

source

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

p.comp f ≤ q.comp f

source

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

p.comp f ≤ q.comp f

source

theorem group_seminorm.comp_mul_le {E : Type u_4} {F : Type u_5} [comm_group E] [comm_group F] (p : group_seminorm E) (f g : F →* E) :

p.comp (f * g) ≤ p.comp f + p.comp g

source

theorem add_group_seminorm.comp_add_le {E : Type u_4} {F : Type u_5} [add_comm_group E] [add_comm_group F] (p : add_group_seminorm E) (f g : F →+ E) :

p.comp (f + g) ≤ p.comp f + p.comp g

source

theorem group_seminorm.mul_bdd_below_range_add {E : Type u_4} [comm_group E] {p q : group_seminorm E} {x : E} :

bdd_below (set.range (λ (y : E), ⇑p y + ⇑q (x / y)))

source

theorem add_group_seminorm.add_bdd_below_range_add {E : Type u_4} [add_comm_group E] {p q : add_group_seminorm E} {x : E} :

bdd_below (set.range (λ (y : E), ⇑p y + ⇑q (x - y)))

source

@[protected, instance]

noncomputable def add_group_seminorm.has_inf {E : Type u_4} [add_comm_group E] :

has_inf (add_group_seminorm E)

Equations

add_group_seminorm.has_inf = {inf := λ (p q : add_group_seminorm E), {to_fun := λ (x : E), ⨅ (y : E), ⇑p y + ⇑q (x - y), map_zero' := _, add_le' := _, neg' := _}}

source

@[protected, instance]

noncomputable def group_seminorm.has_inf {E : Type u_4} [comm_group E] :

has_inf (group_seminorm E)

Equations

group_seminorm.has_inf = {inf := λ (p q : group_seminorm E), {to_fun := λ (x : E), ⨅ (y : E), ⇑p y + ⇑q (x / y), map_one' := _, mul_le' := _, inv' := _}}

source

@[simp]

theorem group_seminorm.inf_apply {E : Type u_4} [comm_group E] (p q : group_seminorm E) (x : E) :

⇑(p ⊓ q) x = ⨅ (y : E), ⇑p y + ⇑q (x / y)

source

@[simp]

theorem add_group_seminorm.inf_apply {E : Type u_4} [add_comm_group E] (p q : add_group_seminorm E) (x : E) :

⇑(p ⊓ q) x = ⨅ (y : E), ⇑p y + ⇑q (x - y)

source

@[protected, instance]

noncomputable def group_seminorm.lattice {E : Type u_4} [comm_group E] :

lattice (group_seminorm E)

Equations

group_seminorm.lattice = {sup := semilattice_sup.sup group_seminorm.semilattice_sup, le := semilattice_sup.le group_seminorm.semilattice_sup, lt := semilattice_sup.lt group_seminorm.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf group_seminorm.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

noncomputable def add_group_seminorm.lattice {E : Type u_4} [add_comm_group E] :

lattice (add_group_seminorm E)

Equations

add_group_seminorm.lattice = {sup := semilattice_sup.sup add_group_seminorm.semilattice_sup, le := semilattice_sup.le add_group_seminorm.semilattice_sup, lt := semilattice_sup.lt add_group_seminorm.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf add_group_seminorm.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def add_group_seminorm.has_one {E : Type u_4} [add_group E] [decidable_eq E] :

has_one (add_group_seminorm E)

Equations

add_group_seminorm.has_one = {one := {to_fun := λ (x : E), ite (x = 0) 0 1, map_zero' := _, add_le' := _, neg' := _}}

source

@[simp]

theorem add_group_seminorm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def add_group_seminorm.has_smul {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] :

has_smul R (add_group_seminorm E)

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

Equations

add_group_seminorm.has_smul = {smul := λ (r : R) (p : add_group_seminorm E), {to_fun := λ (x : E), r • ⇑p x, map_zero' := _, add_le' := _, neg' := _}}

source

@[simp, norm_cast]

theorem add_group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : add_group_seminorm E) :

⇑(r • p) = r • ⇑p

source

@[simp]

theorem add_group_seminorm.smul_apply {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : add_group_seminorm E) (x : E) :

⇑(r • p) x = r • ⇑p x

source

@[protected, instance]

def add_group_seminorm.is_scalar_tower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] [has_smul R' ℝ] [has_smul R' nnreal] [is_scalar_tower R' nnreal ℝ] [has_smul R R'] [is_scalar_tower R R' ℝ] :

is_scalar_tower R R' (add_group_seminorm E)

source

theorem add_group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p q : add_group_seminorm E) :

r • (p ⊔ q) = r • p ⊔ r • q

source

@[protected, instance]

def nonarch_add_group_seminorm.nonarch_add_group_seminorm_class {E : Type u_4} [add_group E] :

nonarch_add_group_seminorm_class (nonarch_add_group_seminorm E) E

Equations

nonarch_add_group_seminorm.nonarch_add_group_seminorm_class = {coe := λ (f : nonarch_add_group_seminorm E), f.to_fun, coe_injective' := _, map_add_le_max := _, map_zero := _, map_neg_eq_map' := _}

source

@[protected, instance]

def nonarch_add_group_seminorm.has_coe_to_fun {E : Type u_4} [add_group E] :

has_coe_to_fun (nonarch_add_group_seminorm E) (λ (_x : nonarch_add_group_seminorm E), E → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

nonarch_add_group_seminorm.has_coe_to_fun = {coe := nonarch_add_group_seminorm.to_fun _inst_1}

source

@[simp]

theorem nonarch_add_group_seminorm.to_fun_eq_coe {E : Type u_4} [add_group E] {p : nonarch_add_group_seminorm E} :

p.to_fun = ⇑p

source

@[ext]

theorem nonarch_add_group_seminorm.ext {E : Type u_4} [add_group E] {p q : nonarch_add_group_seminorm E} :

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

source

@[protected, instance]

noncomputable def nonarch_add_group_seminorm.partial_order {E : Type u_4} [add_group E] :

partial_order (nonarch_add_group_seminorm E)

Equations

nonarch_add_group_seminorm.partial_order = partial_order.lift coe_fn nonarch_add_group_seminorm.partial_order._proof_1

source

theorem nonarch_add_group_seminorm.le_def {E : Type u_4} [add_group E] {p q : nonarch_add_group_seminorm E} :

p ≤ q ↔ ⇑p ≤ ⇑q

source

theorem nonarch_add_group_seminorm.lt_def {E : Type u_4} [add_group E] {p q : nonarch_add_group_seminorm E} :

p < q ↔ ⇑p < ⇑q

source

@[simp, norm_cast]

theorem nonarch_add_group_seminorm.coe_le_coe {E : Type u_4} [add_group E] {p q : nonarch_add_group_seminorm E} :

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp, norm_cast]

theorem nonarch_add_group_seminorm.coe_lt_coe {E : Type u_4} [add_group E] {p q : nonarch_add_group_seminorm E} :

⇑p < ⇑q ↔ p < q

source

@[protected, instance]

def nonarch_add_group_seminorm.has_zero {E : Type u_4} [add_group E] :

has_zero (nonarch_add_group_seminorm E)

Equations

nonarch_add_group_seminorm.has_zero = {zero := {to_fun := 0, map_zero' := _, add_le_max' := _, neg' := _}}

source

@[simp, norm_cast]

theorem nonarch_add_group_seminorm.coe_zero {E : Type u_4} [add_group E] :

⇑0 = 0

source

@[simp]

theorem nonarch_add_group_seminorm.zero_apply {E : Type u_4} [add_group E] (x : E) :

⇑0 x = 0

source

@[protected, instance]

def nonarch_add_group_seminorm.inhabited {E : Type u_4} [add_group E] :

inhabited (nonarch_add_group_seminorm E)

Equations

nonarch_add_group_seminorm.inhabited = {default := 0}

source

@[protected, instance]

def nonarch_add_group_seminorm.has_sup {E : Type u_4} [add_group E] :

has_sup (nonarch_add_group_seminorm E)

Equations

nonarch_add_group_seminorm.has_sup = {sup := λ (p q : nonarch_add_group_seminorm E), {to_fun := ⇑p ⊔ ⇑q, map_zero' := _, add_le_max' := _, neg' := _}}

source

@[simp, norm_cast]

theorem nonarch_add_group_seminorm.coe_sup {E : Type u_4} [add_group E] (p q : nonarch_add_group_seminorm E) :

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

source

@[simp]

theorem nonarch_add_group_seminorm.sup_apply {E : Type u_4} [add_group E] (p q : nonarch_add_group_seminorm E) (x : E) :

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

source

@[protected, instance]

noncomputable def nonarch_add_group_seminorm.semilattice_sup {E : Type u_4} [add_group E] :

semilattice_sup (nonarch_add_group_seminorm E)

Equations

nonarch_add_group_seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn nonarch_add_group_seminorm.semilattice_sup._proof_1 nonarch_add_group_seminorm.coe_sup

source

theorem nonarch_add_group_seminorm.add_bdd_below_range_add {E : Type u_4} [add_comm_group E] {p q : nonarch_add_group_seminorm E} {x : E} :

bdd_below (set.range (λ (y : E), ⇑p y + ⇑q (x - y)))

source

@[protected, instance]

def group_seminorm.has_one {E : Type u_4} [group E] [decidable_eq E] :

has_one (group_seminorm E)

Equations

group_seminorm.has_one = {one := {to_fun := λ (x : E), ite (x = 1) 0 1, map_one' := _, mul_le' := _, inv' := _}}

source

@[simp]

theorem group_seminorm.apply_one {E : Type u_4} [group E] [decidable_eq E] (x : E) :

⇑1 x = ite (x = 1) 0 1

source

@[protected, instance]

def group_seminorm.has_smul {R : Type u_2} {E : Type u_4} [group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] :

has_smul R (group_seminorm E)

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

Equations

group_seminorm.has_smul = {smul := λ (r : R) (p : group_seminorm E), {to_fun := λ (x : E), r • ⇑p x, map_one' := _, mul_le' := _, inv' := _}}

source

@[protected, instance]

def group_seminorm.is_scalar_tower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] [has_smul R' ℝ] [has_smul R' nnreal] [is_scalar_tower R' nnreal ℝ] [has_smul R R'] [is_scalar_tower R R' ℝ] :

is_scalar_tower R R' (group_seminorm E)

source

@[simp, norm_cast]

theorem group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : group_seminorm E) :

⇑(r • p) = r • ⇑p

source

@[simp]

theorem group_seminorm.smul_apply {R : Type u_2} {E : Type u_4} [group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : group_seminorm E) (x : E) :

⇑(r • p) x = r • ⇑p x

source

theorem group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p q : group_seminorm E) :

r • (p ⊔ q) = r • p ⊔ r • q

source

@[protected, instance]

def nonarch_add_group_seminorm.has_one {E : Type u_4} [add_group E] [decidable_eq E] :

has_one (nonarch_add_group_seminorm E)

Equations

nonarch_add_group_seminorm.has_one = {one := {to_fun := λ (x : E), ite (x = 0) 0 1, map_zero' := _, add_le_max' := _, neg' := _}}

source

@[simp]

theorem nonarch_add_group_seminorm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def nonarch_add_group_seminorm.has_smul {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] :

has_smul R (nonarch_add_group_seminorm E)

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

Equations

nonarch_add_group_seminorm.has_smul = {smul := λ (r : R) (p : nonarch_add_group_seminorm E), {to_fun := λ (x : E), r • ⇑p x, map_zero' := _, add_le_max' := _, neg' := _}}

source

@[protected, instance]

def nonarch_add_group_seminorm.is_scalar_tower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] [has_smul R' ℝ] [has_smul R' nnreal] [is_scalar_tower R' nnreal ℝ] [has_smul R R'] [is_scalar_tower R R' ℝ] :

is_scalar_tower R R' (nonarch_add_group_seminorm E)

source

@[simp, norm_cast]

theorem nonarch_add_group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : nonarch_add_group_seminorm E) :

⇑(r • p) = r • ⇑p

source

@[simp]

theorem nonarch_add_group_seminorm.smul_apply {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : nonarch_add_group_seminorm E) (x : E) :

⇑(r • p) x = r • ⇑p x

source

theorem nonarch_add_group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p q : nonarch_add_group_seminorm E) :

r • (p ⊔ q) = r • p ⊔ r • q

source

@[protected, instance]

def group_norm.group_norm_class {E : Type u_4} [group E] :

group_norm_class (group_norm E) E ℝ

Equations

group_norm.group_norm_class = {coe := λ (f : group_norm E), f.to_fun, coe_injective' := _, map_mul_le_add := _, map_one_eq_zero := _, map_inv_eq_map := _, eq_one_of_map_eq_zero := _}

source

@[protected, instance]

def add_group_norm.add_group_norm_class {E : Type u_4} [add_group E] :

add_group_norm_class (add_group_norm E) E ℝ

Equations

add_group_norm.add_group_norm_class = {coe := λ (f : add_group_norm E), f.to_fun, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, eq_zero_of_map_eq_zero := _}

source

@[protected, instance]

def group_norm.has_coe_to_fun {E : Type u_4} [group E] :

has_coe_to_fun (group_norm E) (λ (_x : group_norm E), E → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

group_norm.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[protected, instance]

def add_group_norm.has_coe_to_fun {E : Type u_4} [add_group E] :

has_coe_to_fun (add_group_norm E) (λ (_x : add_group_norm E), E → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

add_group_norm.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem group_norm.to_fun_eq_coe {E : Type u_4} [group E] {p : group_norm E} :

p.to_fun = ⇑p

source

@[simp]

theorem add_group_norm.to_fun_eq_coe {E : Type u_4} [add_group E] {p : add_group_norm E} :

p.to_fun = ⇑p

source

@[ext]

theorem add_group_norm.ext {E : Type u_4} [add_group E] {p q : add_group_norm E} :

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

source

@[ext]

theorem group_norm.ext {E : Type u_4} [group E] {p q : group_norm E} :

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

source

@[protected, instance]

def add_group_norm.partial_order {E : Type u_4} [add_group E] :

partial_order (add_group_norm E)

Equations

add_group_norm.partial_order = partial_order.lift coe_fn add_group_norm.partial_order._proof_1

source

@[protected, instance]

def group_norm.partial_order {E : Type u_4} [group E] :

partial_order (group_norm E)

Equations

group_norm.partial_order = partial_order.lift coe_fn group_norm.partial_order._proof_1

source

theorem group_norm.le_def {E : Type u_4} [group E] {p q : group_norm E} :

p ≤ q ↔ ⇑p ≤ ⇑q

source

theorem add_group_norm.le_def {E : Type u_4} [add_group E] {p q : add_group_norm E} :

p ≤ q ↔ ⇑p ≤ ⇑q

source

theorem group_norm.lt_def {E : Type u_4} [group E] {p q : group_norm E} :

p < q ↔ ⇑p < ⇑q

source

theorem add_group_norm.lt_def {E : Type u_4} [add_group E] {p q : add_group_norm E} :

p < q ↔ ⇑p < ⇑q

source

@[simp, norm_cast]

theorem group_norm.coe_le_coe {E : Type u_4} [group E] {p q : group_norm E} :

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp]

theorem add_group_norm.coe_le_coe {E : Type u_4} [add_group E] {p q : add_group_norm E} :

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp, norm_cast]

theorem group_norm.coe_lt_coe {E : Type u_4} [group E] {p q : group_norm E} :

⇑p < ⇑q ↔ p < q

source

@[simp]

theorem add_group_norm.coe_lt_coe {E : Type u_4} [add_group E] {p q : add_group_norm E} :

⇑p < ⇑q ↔ p < q

source

@[protected, instance]

def group_norm.has_add {E : Type u_4} [group E] :

has_add (group_norm E)

Equations

group_norm.has_add = {add := λ (p q : group_norm E), {to_fun := (p.to_group_seminorm + q.to_group_seminorm).to_fun, map_one' := _, mul_le' := _, inv' := _, eq_one_of_map_eq_zero' := _}}

source

@[protected, instance]

def add_group_norm.has_add {E : Type u_4} [add_group E] :

has_add (add_group_norm E)

Equations

add_group_norm.has_add = {add := λ (p q : add_group_norm E), {to_fun := (p.to_add_group_seminorm + q.to_add_group_seminorm).to_fun, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}}

source

@[simp]

theorem add_group_norm.coe_add {E : Type u_4} [add_group E] (p q : add_group_norm E) :

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

source

@[simp]

theorem group_norm.coe_add {E : Type u_4} [group E] (p q : group_norm E) :

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

source

@[simp]

theorem group_norm.add_apply {E : Type u_4} [group E] (p q : group_norm E) (x : E) :

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

source

@[simp]

theorem add_group_norm.add_apply {E : Type u_4} [add_group E] (p q : add_group_norm E) (x : E) :

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

source

@[protected, instance]

def add_group_norm.has_sup {E : Type u_4} [add_group E] :

has_sup (add_group_norm E)

Equations

add_group_norm.has_sup = {sup := λ (p q : add_group_norm E), {to_fun := (p.to_add_group_seminorm ⊔ q.to_add_group_seminorm).to_fun, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}}

source

@[protected, instance]

def group_norm.has_sup {E : Type u_4} [group E] :

has_sup (group_norm E)

Equations

group_norm.has_sup = {sup := λ (p q : group_norm E), {to_fun := (p.to_group_seminorm ⊔ q.to_group_seminorm).to_fun, map_one' := _, mul_le' := _, inv' := _, eq_one_of_map_eq_zero' := _}}

source

@[simp, norm_cast]

theorem group_norm.coe_sup {E : Type u_4} [group E] (p q : group_norm E) :

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

source

@[simp]

theorem add_group_norm.coe_sup {E : Type u_4} [add_group E] (p q : add_group_norm E) :

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

source

@[simp]

theorem add_group_norm.sup_apply {E : Type u_4} [add_group E] (p q : add_group_norm E) (x : E) :

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

source

@[simp]

theorem group_norm.sup_apply {E : Type u_4} [group E] (p q : group_norm E) (x : E) :

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

source

@[protected, instance]

def add_group_norm.semilattice_sup {E : Type u_4} [add_group E] :

semilattice_sup (add_group_norm E)

Equations

add_group_norm.semilattice_sup = function.injective.semilattice_sup coe_fn add_group_norm.semilattice_sup._proof_1 add_group_norm.coe_sup

source

@[protected, instance]

def group_norm.semilattice_sup {E : Type u_4} [group E] :

semilattice_sup (group_norm E)

Equations

group_norm.semilattice_sup = function.injective.semilattice_sup coe_fn group_norm.semilattice_sup._proof_1 group_norm.coe_sup

source

@[protected, instance]

def add_group_norm.has_one {E : Type u_4} [add_group E] [decidable_eq E] :

has_one (add_group_norm E)

Equations

add_group_norm.has_one = {one := {to_fun := 1.to_fun, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}}

source

@[simp]

theorem add_group_norm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def add_group_norm.inhabited {E : Type u_4} [add_group E] [decidable_eq E] :

inhabited (add_group_norm E)

Equations

add_group_norm.inhabited = {default := 1}

source

@[protected, instance]

def group_norm.has_one {E : Type u_4} [group E] [decidable_eq E] :

has_one (group_norm E)

Equations

group_norm.has_one = {one := {to_fun := 1.to_fun, map_one' := _, mul_le' := _, inv' := _, eq_one_of_map_eq_zero' := _}}

source

@[simp]

theorem group_norm.apply_one {E : Type u_4} [group E] [decidable_eq E] (x : E) :

⇑1 x = ite (x = 1) 0 1

source

@[protected, instance]

def group_norm.inhabited {E : Type u_4} [group E] [decidable_eq E] :

inhabited (group_norm E)

Equations

group_norm.inhabited = {default := 1}

source

@[protected, instance]

def nonarch_add_group_norm.nonarch_add_group_norm_class {E : Type u_4} [add_group E] :

nonarch_add_group_norm_class (nonarch_add_group_norm E) E

Equations

nonarch_add_group_norm.nonarch_add_group_norm_class = {coe := λ (f : nonarch_add_group_norm E), f.to_fun, coe_injective' := _, map_add_le_max := _, map_zero := _, map_neg_eq_map' := _, eq_zero_of_map_eq_zero := _}

source

@[protected, instance]

noncomputable def nonarch_add_group_norm.has_coe_to_fun {E : Type u_4} [add_group E] :

has_coe_to_fun (nonarch_add_group_norm E) (λ (_x : nonarch_add_group_norm E), E → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

nonarch_add_group_norm.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem nonarch_add_group_norm.to_fun_eq_coe {E : Type u_4} [add_group E] {p : nonarch_add_group_norm E} :

p.to_fun = ⇑p

source

@[ext]

theorem nonarch_add_group_norm.ext {E : Type u_4} [add_group E] {p q : nonarch_add_group_norm E} :

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

source

@[protected, instance]

noncomputable def nonarch_add_group_norm.partial_order {E : Type u_4} [add_group E] :

partial_order (nonarch_add_group_norm E)

Equations

nonarch_add_group_norm.partial_order = partial_order.lift coe_fn nonarch_add_group_norm.partial_order._proof_1

source

theorem nonarch_add_group_norm.le_def {E : Type u_4} [add_group E] {p q : nonarch_add_group_norm E} :

p ≤ q ↔ ⇑p ≤ ⇑q

source

theorem nonarch_add_group_norm.lt_def {E : Type u_4} [add_group E] {p q : nonarch_add_group_norm E} :

p < q ↔ ⇑p < ⇑q

source

@[simp, norm_cast]

theorem nonarch_add_group_norm.coe_le_coe {E : Type u_4} [add_group E] {p q : nonarch_add_group_norm E} :

⇑p ≤ ⇑q ↔ p ≤ q

source

@[simp, norm_cast]

theorem nonarch_add_group_norm.coe_lt_coe {E : Type u_4} [add_group E] {p q : nonarch_add_group_norm E} :

⇑p < ⇑q ↔ p < q

source

@[protected, instance]

def nonarch_add_group_norm.has_sup {E : Type u_4} [add_group E] :

has_sup (nonarch_add_group_norm E)

Equations

nonarch_add_group_norm.has_sup = {sup := λ (p q : nonarch_add_group_norm E), {to_fun := (p.to_nonarch_add_group_seminorm ⊔ q.to_nonarch_add_group_seminorm).to_fun, map_zero' := _, add_le_max' := _, neg' := _, eq_zero_of_map_eq_zero' := _}}

source

@[simp, norm_cast]

theorem nonarch_add_group_norm.coe_sup {E : Type u_4} [add_group E] (p q : nonarch_add_group_norm E) :

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

source

@[simp]

theorem nonarch_add_group_norm.sup_apply {E : Type u_4} [add_group E] (p q : nonarch_add_group_norm E) (x : E) :

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

source

@[protected, instance]

noncomputable def nonarch_add_group_norm.semilattice_sup {E : Type u_4} [add_group E] :

semilattice_sup (nonarch_add_group_norm E)

Equations

nonarch_add_group_norm.semilattice_sup = function.injective.semilattice_sup coe_fn nonarch_add_group_norm.semilattice_sup._proof_1 nonarch_add_group_norm.coe_sup

source

@[protected, instance]

def nonarch_add_group_norm.has_one {E : Type u_4} [add_group E] [decidable_eq E] :

has_one (nonarch_add_group_norm E)

Equations

nonarch_add_group_norm.has_one = {one := {to_fun := 1.to_fun, map_zero' := _, add_le_max' := _, neg' := _, eq_zero_of_map_eq_zero' := _}}

source

@[simp]

theorem nonarch_add_group_norm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def nonarch_add_group_norm.inhabited {E : Type u_4} [add_group E] [decidable_eq E] :

inhabited (nonarch_add_group_norm E)

Equations

nonarch_add_group_norm.inhabited = {default := 1}

mathlib3 documentation

Group seminorms #

Main declarations #

Notes #

References #

Tags #

Seminorms #

Norms #