Group seminorms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
add_group_seminorm: A functionffrom an additive groupGto the reals that preserves zero, takes nonnegative values, is subadditive and such thatf (-x) = f xfor allx.nonarch_add_group_seminorm: A functionffrom an additive groupGto the reals that preserves zero, takes nonnegative values, is nonarchimedean and such thatf (-x) = f xfor allx.group_seminorm: A functionffrom a groupGto the reals that sends one to zero, takes nonnegative values, is submultiplicative and such thatf x⁻¹ = f xfor allx.add_group_norm: A seminormfsuch thatf x = 0 → x = 0for allx.nonarch_add_group_norm: A nonarchimedean seminormfsuch thatf x = 0 → x = 0for allx.group_norm: A seminormfsuch thatf x = 0 → x = 1for allx.
Notes #
The corresponding hom classes are defined in analysis.order.hom.basic to be used by absolute
values.
We do not define nonarch_add_group_seminorm as an extension of add_group_seminorm to avoid
having a superfluous add_le' field in the resulting structure. The same applies to
nonarch_add_group_norm.
References #
Tags #
norm, seminorm
@[nolint]
- 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
- add_group_seminorm.has_sizeof_inst
- add_group_seminorm.add_group_seminorm_class
- add_group_seminorm.has_coe_to_fun
- add_group_seminorm.partial_order
- add_group_seminorm.has_zero
- add_group_seminorm.inhabited
- add_group_seminorm.has_add
- add_group_seminorm.has_sup
- add_group_seminorm.semilattice_sup
- add_group_seminorm.has_inf
- add_group_seminorm.lattice
- add_group_seminorm.has_one
- add_group_seminorm.has_smul
- add_group_seminorm.is_scalar_tower
- 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
- group_seminorm.has_sizeof_inst
- group_seminorm.group_seminorm_class
- group_seminorm.has_coe_to_fun
- group_seminorm.partial_order
- group_seminorm.has_zero
- group_seminorm.inhabited
- group_seminorm.has_add
- group_seminorm.has_sup
- group_seminorm.semilattice_sup
- group_seminorm.has_inf
- group_seminorm.lattice
- group_seminorm.has_one
- group_seminorm.has_smul
- group_seminorm.is_scalar_tower
@[nolint]
def
nonarch_add_group_seminorm.to_zero_hom
{G : Type u_7}
[add_group G]
(self : nonarch_add_group_seminorm G) :
- 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
- nonarch_add_group_seminorm.has_sizeof_inst
- nonarch_add_group_seminorm.nonarch_add_group_seminorm_class
- nonarch_add_group_seminorm.has_coe_to_fun
- nonarch_add_group_seminorm.partial_order
- nonarch_add_group_seminorm.has_zero
- nonarch_add_group_seminorm.inhabited
- nonarch_add_group_seminorm.has_sup
- nonarch_add_group_seminorm.semilattice_sup
- nonarch_add_group_seminorm.has_one
- nonarch_add_group_seminorm.has_smul
- nonarch_add_group_seminorm.is_scalar_tower
NOTE: We do not define nonarch_add_group_seminorm as an extension of add_group_seminorm
to avoid having a superfluous add_le' field in the resulting structure. The same applies to
nonarch_add_group_norm below.
- 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
@[nolint]
@[nolint]
- 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
@[nolint]
def
nonarch_add_group_norm.to_nonarch_add_group_seminorm
{G : Type u_7}
[add_group G]
(self : nonarch_add_group_norm G) :
- 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
@[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
@[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 α] :
@[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
Instances of other typeclasses for nonarch_add_group_norm_class
- nonarch_add_group_norm_class.has_sizeof_inst
@[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 α] :
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) :
@[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] :
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 := _}
@[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] :
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 := _}
Seminorms #
@[protected, instance]
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 := _}
@[protected, instance]
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 := _}
@[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
@[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}
@[simp]
@[simp]
@[ext]
@[ext]
@[protected, instance]
Equations
- add_group_seminorm.partial_order = partial_order.lift coe_fn add_group_seminorm.partial_order._proof_1
@[protected, instance]
Equations
- group_seminorm.partial_order = partial_order.lift coe_fn group_seminorm.partial_order._proof_1
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp]
@[protected, instance]
@[protected, instance]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[simp]
theorem
add_group_seminorm.add_apply
{E : Type u_4}
[add_group E]
(p q : add_group_seminorm E)
(x : E) :
@[simp]
@[protected, instance]
@[protected, instance]
@[simp]
@[simp, norm_cast]
@[simp]
theorem
add_group_seminorm.sup_apply
{E : Type u_4}
[add_group E]
(p q : add_group_seminorm E)
(x : E) :
@[simp]
@[protected, instance]
Equations
- group_seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn group_seminorm.semilattice_sup._proof_1 group_seminorm.coe_sup
@[protected, instance]
Equations
- add_group_seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn add_group_seminorm.semilattice_sup._proof_1 add_group_seminorm.coe_sup
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) :
Composition of an additive group seminorm with an additive monoid homomorphism as an additive group seminorm.
def
group_seminorm.comp
{E : Type u_4}
{F : Type u_5}
[group E]
[group F]
(p : group_seminorm E)
(f : F →* E) :
Composition of a group seminorm with a monoid homomorphism as a group seminorm.
@[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
@[simp]
theorem
group_seminorm.comp_id
{E : Type u_4}
[group E]
(p : group_seminorm E) :
p.comp (monoid_hom.id E) = p
@[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) :
@[simp]
theorem
group_seminorm.comp_zero
{E : Type u_4}
{F : Type u_5}
[group E]
[group F]
(p : group_seminorm E) :
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) :
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) :
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) :
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) :
theorem
group_seminorm.mul_bdd_below_range_add
{E : Type u_4}
[comm_group E]
{p q : group_seminorm E}
{x : E} :
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} :
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
theorem
add_group_seminorm.inf_apply
{E : Type u_4}
[add_comm_group E]
(p q : add_group_seminorm E)
(x : E) :
@[protected, instance]
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 := _}
@[protected, instance]
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 := _}
@[protected, instance]
@[simp]
@[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.
@[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)
@[protected, instance]
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' := _}
@[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
@[simp]
theorem
nonarch_add_group_seminorm.to_fun_eq_coe
{E : Type u_4}
[add_group E]
{p : nonarch_add_group_seminorm E} :
@[ext]
theorem
nonarch_add_group_seminorm.ext
{E : Type u_4}
[add_group E]
{p q : nonarch_add_group_seminorm E} :
@[protected, instance]
Equations
- nonarch_add_group_seminorm.partial_order = partial_order.lift coe_fn nonarch_add_group_seminorm.partial_order._proof_1
theorem
nonarch_add_group_seminorm.le_def
{E : Type u_4}
[add_group E]
{p q : nonarch_add_group_seminorm E} :
theorem
nonarch_add_group_seminorm.lt_def
{E : Type u_4}
[add_group E]
{p q : nonarch_add_group_seminorm E} :
@[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} :
@[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} :
@[protected, instance]
Equations
- nonarch_add_group_seminorm.has_zero = {zero := {to_fun := 0, map_zero' := _, add_le_max' := _, neg' := _}}
@[simp, norm_cast]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
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' := _}}
@[simp, norm_cast]
theorem
nonarch_add_group_seminorm.coe_sup
{E : Type u_4}
[add_group E]
(p q : nonarch_add_group_seminorm E) :
@[simp]
theorem
nonarch_add_group_seminorm.sup_apply
{E : Type u_4}
[add_group E]
(p q : nonarch_add_group_seminorm E)
(x : E) :
@[protected, instance]
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
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} :
@[protected, instance]
@[simp]
@[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.
@[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)
@[protected, instance]
@[simp]
theorem
nonarch_add_group_seminorm.apply_one
{E : Type u_4}
[add_group E]
[decidable_eq E]
(x : E) :
@[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 ℝ] :
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' := _}}
@[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' ℝ] :
Norms #
@[protected, instance]
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 := _}
@[protected, instance]
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 := _}
@[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.
@[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.
@[simp]
@[simp]
@[ext]
@[ext]
@[protected, instance]
Equations
- add_group_norm.partial_order = partial_order.lift coe_fn add_group_norm.partial_order._proof_1
@[protected, instance]
Equations
- group_norm.partial_order = partial_order.lift coe_fn group_norm.partial_order._proof_1
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp]
@[protected, instance]
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' := _}}
@[protected, instance]
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' := _}}
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
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' := _}}
@[protected, instance]
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' := _}}
@[simp, norm_cast]
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
- add_group_norm.semilattice_sup = function.injective.semilattice_sup coe_fn add_group_norm.semilattice_sup._proof_1 add_group_norm.coe_sup
@[protected, instance]
Equations
- group_norm.semilattice_sup = function.injective.semilattice_sup coe_fn group_norm.semilattice_sup._proof_1 group_norm.coe_sup
@[protected, instance]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
@[simp]
@[protected, instance]
Equations
- group_norm.inhabited = {default := 1}
@[protected, instance]
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 := _}
@[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.
@[simp]
theorem
nonarch_add_group_norm.to_fun_eq_coe
{E : Type u_4}
[add_group E]
{p : nonarch_add_group_norm E} :
@[ext]
@[protected, instance]
Equations
- nonarch_add_group_norm.partial_order = partial_order.lift coe_fn nonarch_add_group_norm.partial_order._proof_1
theorem
nonarch_add_group_norm.le_def
{E : Type u_4}
[add_group E]
{p q : nonarch_add_group_norm E} :
theorem
nonarch_add_group_norm.lt_def
{E : Type u_4}
[add_group E]
{p q : nonarch_add_group_norm E} :
@[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} :
@[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} :
@[protected, instance]
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' := _}}
@[simp, norm_cast]
theorem
nonarch_add_group_norm.coe_sup
{E : Type u_4}
[add_group E]
(p q : nonarch_add_group_norm E) :
@[simp]
theorem
nonarch_add_group_norm.sup_apply
{E : Type u_4}
[add_group E]
(p q : nonarch_add_group_norm E)
(x : E) :
@[protected, instance]
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
@[protected, instance]
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' := _}}
@[simp]
@[protected, instance]