mathlib3 documentation

analysis.normed.group.basic

Normed (semi)groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define 10 classes:

We also prove basic properties of (semi)normed groups and provide some instances.

Notes #

The current convention dist x y = ‖x - y‖ means that the distance is invariant under right addition, but actions in mathlib are usually from the left. This means we might want to change it to dist x y = ‖-x + y‖.

The normed group hierarchy would lend itself well to a mixin design (that is, having seminormed_group and seminormed_add_group not extend group and add_group), but we choose not to for performance concerns.

Tags #

normed group

source
@[class]
structure has_norm (E : Type u_9) :
Type u_9

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This class is designed to be extended in more interesting classes specifying the properties of the norm.

Instances of this typeclass
Instances of other typeclasses for has_norm
  • has_norm.has_sizeof_inst
source
@[class]
structure has_nnnorm (E : Type u_9) :
Type u_9

Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ‖x‖₊.

Instances of this typeclass
Instances of other typeclasses for has_nnnorm
  • has_nnnorm.has_sizeof_inst
source
@[class]
structure seminormed_add_group (E : Type u_9) :
Type u_9

A seminormed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a pseudometric space structure.

Instances of this typeclass
Instances of other typeclasses for seminormed_add_group
  • seminormed_add_group.has_sizeof_inst
source
@[class]
structure seminormed_group (E : Type u_9) :
Type u_9

A seminormed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a pseudometric space structure.

Instances of this typeclass
Instances of other typeclasses for seminormed_group
  • seminormed_group.has_sizeof_inst
source
@[class]
structure normed_add_group (E : Type u_9) :
Type u_9

A normed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a metric space structure.

Instances of this typeclass
Instances of other typeclasses for normed_add_group
  • normed_add_group.has_sizeof_inst
source
@[class]
structure normed_group (E : Type u_9) :
Type u_9

A normed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a metric space structure.

Instances of this typeclass
Instances of other typeclasses for normed_group
  • normed_group.has_sizeof_inst
source
@[class]
structure seminormed_add_comm_group (E : Type u_9) :
Type u_9

A seminormed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a pseudometric space structure.

Instances of this typeclass
Instances of other typeclasses for seminormed_add_comm_group
  • seminormed_add_comm_group.has_sizeof_inst
source
@[class]
structure seminormed_comm_group (E : Type u_9) :
Type u_9

A seminormed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a pseudometric space structure.

Instances of this typeclass
Instances of other typeclasses for seminormed_comm_group
  • seminormed_comm_group.has_sizeof_inst
source
@[class]
structure normed_add_comm_group (E : Type u_9) :
Type u_9

A normed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a metric space structure.

Instances of this typeclass
Instances of other typeclasses for normed_add_comm_group
  • normed_add_comm_group.has_sizeof_inst
source
@[class]
structure normed_comm_group (E : Type u_9) :
Type u_9

A normed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a metric space structure.

Instances of this typeclass
Instances of other typeclasses for normed_comm_group
  • normed_comm_group.has_sizeof_inst
source
@[protected, instance]
def normed_group.to_seminormed_group {E : Type u_6} [normed_group E] :
seminormed_group E
Equations
source
@[protected, instance]
def normed_add_group.to_seminormed_add_group {E : Type u_6} [normed_add_group E] :
seminormed_add_group E
Equations
source
@[protected, instance]
def normed_comm_group.to_seminormed_comm_group {E : Type u_6} [normed_comm_group E] :
seminormed_comm_group E
Equations
source
@[protected, instance]
def normed_add_comm_group.to_seminormed_add_comm_group {E : Type u_6} [normed_add_comm_group E] :
seminormed_add_comm_group E
Equations
source
@[protected, instance]
def seminormed_add_comm_group.to_seminormed_add_group {E : Type u_6} [seminormed_add_comm_group E] :
seminormed_add_group E
Equations
source
@[protected, instance]
def seminormed_comm_group.to_seminormed_group {E : Type u_6} [seminormed_comm_group E] :
seminormed_group E
Equations
source
@[protected, instance]
def normed_comm_group.to_normed_group {E : Type u_6} [normed_comm_group E] :
normed_group E
Equations
source
@[protected, instance]
def normed_add_comm_group.to_normed_add_group {E : Type u_6} [normed_add_comm_group E] :
normed_add_group E
Equations
source
@[reducible]
def normed_group.of_separation {E : Type u_6} [seminormed_group E] (h : ∀ (x : E), ‖x‖ = 0 → x = 1) :
normed_group E

Construct a normed_group from a seminormed_group satisfying ∀ x, ‖x‖ = 0 → x = 1. This avoids having to go back to the (pseudo_)metric_space level when declaring a normed_group instance as a special case of a more general seminormed_group instance.

Equations
source
def normed_add_group.of_separation {E : Type u_6} [seminormed_add_group E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0) :
normed_add_group E

Construct a normed_add_group from a seminormed_add_group satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (pseudo_)metric_space level when declaring a normed_add_group instance as a special case of a more general seminormed_add_group instance.

Equations
source
def normed_add_comm_group.of_separation {E : Type u_6} [seminormed_add_comm_group E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0) :
normed_add_comm_group E

Construct a normed_add_comm_group from a seminormed_add_comm_group satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (pseudo_)metric_space level when declaring a normed_add_comm_group instance as a special case of a more general seminormed_add_comm_group instance.

Equations
source
@[reducible]
def normed_comm_group.of_separation {E : Type u_6} [seminormed_comm_group E] (h : ∀ (x : E), ‖x‖ = 0 → x = 1) :
normed_comm_group E

Construct a normed_comm_group from a seminormed_comm_group satisfying ∀ x, ‖x‖ = 0 → x = 1. This avoids having to go back to the (pseudo_)metric_space level when declaring a normed_comm_group instance as a special case of a more general seminormed_comm_group instance.

Equations
source
def seminormed_add_group.of_add_dist {E : Type u_6} [has_norm E] [add_group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x + z) (y + z)) :
seminormed_add_group E

Construct a seminormed group from a translation-invariant distance.

Equations
source
def seminormed_group.of_mul_dist {E : Type u_6} [has_norm E] [group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x * z) (y * z)) :
seminormed_group E

Construct a seminormed group from a multiplication-invariant distance.

Equations
source
def seminormed_add_group.of_add_dist' {E : Type u_6} [has_norm E] [add_group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist (x + z) (y + z) ≤ has_dist.dist x y) :
seminormed_add_group E

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
source
def seminormed_group.of_mul_dist' {E : Type u_6} [has_norm E] [group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist (x * z) (y * z) ≤ has_dist.dist x y) :
seminormed_group E

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
source
def seminormed_add_comm_group.of_add_dist {E : Type u_6} [has_norm E] [add_comm_group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x + z) (y + z)) :
seminormed_add_comm_group E

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
source
def seminormed_comm_group.of_mul_dist {E : Type u_6} [has_norm E] [comm_group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x * z) (y * z)) :
seminormed_comm_group E

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
source
def seminormed_comm_group.of_mul_dist' {E : Type u_6} [has_norm E] [comm_group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist (x * z) (y * z) ≤ has_dist.dist x y) :
seminormed_comm_group E

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
source
def seminormed_add_comm_group.of_add_dist' {E : Type u_6} [has_norm E] [add_comm_group E] [pseudo_metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist (x + z) (y + z) ≤ has_dist.dist x y) :
seminormed_add_comm_group E

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
source
def normed_group.of_mul_dist {E : Type u_6} [has_norm E] [group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x * z) (y * z)) :
normed_group E

Construct a normed group from a multiplication-invariant distance.

Equations
source
def normed_add_group.of_add_dist {E : Type u_6} [has_norm E] [add_group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x + z) (y + z)) :
normed_add_group E

Construct a normed group from a translation-invariant distance.

Equations
source
def normed_add_group.of_add_dist' {E : Type u_6} [has_norm E] [add_group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist (x + z) (y + z) ≤ has_dist.dist x y) :
normed_add_group E

Construct a normed group from a translation-invariant pseudodistance.

Equations
source
def normed_group.of_mul_dist' {E : Type u_6} [has_norm E] [group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist (x * z) (y * z) ≤ has_dist.dist x y) :
normed_group E

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
source
def normed_comm_group.of_mul_dist {E : Type u_6} [has_norm E] [comm_group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x * z) (y * z)) :
normed_comm_group E

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
source
def normed_add_comm_group.of_add_dist {E : Type u_6} [has_norm E] [add_comm_group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x + z) (y + z)) :
normed_add_comm_group E

Construct a normed group from a translation-invariant pseudodistance.

Equations
source
def normed_add_comm_group.of_add_dist' {E : Type u_6} [has_norm E] [add_comm_group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 0) (h₂ : ∀ (x y z : E), has_dist.dist (x + z) (y + z) ≤ has_dist.dist x y) :
normed_add_comm_group E

Construct a normed group from a translation-invariant pseudodistance.

Equations
source
def normed_comm_group.of_mul_dist' {E : Type u_6} [has_norm E] [comm_group E] [metric_space E] (h₁ : ∀ (x : E), ‖x‖ = has_dist.dist x 1) (h₂ : ∀ (x y z : E), has_dist.dist (x * z) (y * z) ≤ has_dist.dist x y) :
normed_comm_group E

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
source
def add_group_seminorm.to_seminormed_add_group {E : Type u_6} [add_group E] (f : add_group_seminorm E) :
seminormed_add_group E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance* and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def group_seminorm.to_seminormed_group {E : Type u_6} [group E] (f : group_seminorm E) :
seminormed_group E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def group_seminorm.to_seminormed_comm_group {E : Type u_6} [comm_group E] (f : group_seminorm E) :
seminormed_comm_group E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def add_group_seminorm.to_seminormed_add_comm_group {E : Type u_6} [add_comm_group E] (f : add_group_seminorm E) :
seminormed_add_comm_group E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance* and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def group_norm.to_normed_group {E : Type u_6} [group E] (f : group_norm E) :
normed_group E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def add_group_norm.to_normed_add_group {E : Type u_6} [add_group E] (f : add_group_norm E) :
normed_add_group E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def add_group_norm.to_normed_add_comm_group {E : Type u_6} [add_comm_group E] (f : add_group_norm E) :
normed_add_comm_group E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
def group_norm.to_normed_comm_group {E : Type u_6} [comm_group E] (f : group_norm E) :
normed_comm_group E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
@[protected, instance]
def punit.normed_add_comm_group  :
normed_add_comm_group punit
Equations
source
@[simp]
theorem punit.norm_eq_zero (r : punit) :
‖r‖ = 0
source
theorem dist_eq_norm_sub {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist a b = ‖a - b‖
source
theorem dist_eq_norm_div {E : Type u_6} [seminormed_group E] (a b : E) :
has_dist.dist a b = ‖a / b‖
source
theorem dist_eq_norm_sub' {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist a b = ‖b - a‖
source
theorem dist_eq_norm_div' {E : Type u_6} [seminormed_group E] (a b : E) :
has_dist.dist a b = ‖b / a‖
source
theorem dist_eq_norm {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist a b = ‖a - b‖

Alias of dist_eq_norm_sub.

source
theorem dist_eq_norm' {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist a b = ‖b - a‖

Alias of dist_eq_norm_sub'.

source
@[protected, instance]
def normed_group.to_has_isometric_smul_right {E : Type u_6} [seminormed_group E] :
has_isometric_smul Eᵐᵒᵖ E
source
@[protected, instance]
def normed_add_group.to_has_isometric_vadd_right {E : Type u_6} [seminormed_add_group E] :
has_isometric_vadd Eᵃᵒᵖ E
source
@[simp]
theorem dist_one_right {E : Type u_6} [seminormed_group E] (a : E) :
has_dist.dist a 1 = ‖a‖
source
@[simp]
theorem dist_zero_right {E : Type u_6} [seminormed_add_group E] (a : E) :
has_dist.dist a 0 = ‖a‖
source
@[simp]
theorem dist_one_left {E : Type u_6} [seminormed_group E] :
has_dist.dist 1 = has_norm.norm
source
@[simp]
theorem dist_zero_left {E : Type u_6} [seminormed_add_group E] :
has_dist.dist 0 = has_norm.norm
source
theorem isometry.norm_map_of_map_one {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} (hi : isometry f) (h₁ : f 1 = 1) (x : E) :
‖f x‖ = ‖x‖
source
theorem isometry.norm_map_of_map_zero {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} (hi : isometry f) (h₁ : f 0 = 0) (x : E) :
‖f x‖ = ‖x‖
source
theorem tendsto_norm_cocompact_at_top' {E : Type u_6} [seminormed_group E] [proper_space E] :
filter.tendsto has_norm.norm (filter.cocompact E) filter.at_top
source
theorem tendsto_norm_cocompact_at_top {E : Type u_6} [seminormed_add_group E] [proper_space E] :
filter.tendsto has_norm.norm (filter.cocompact E) filter.at_top
source
theorem norm_sub_rev {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a - b‖ = ‖b - a‖
source
theorem norm_div_rev {E : Type u_6} [seminormed_group E] (a b : E) :
‖a / b‖ = ‖b / a‖
source
@[simp]
theorem norm_inv' {E : Type u_6} [seminormed_group E] (a : E) :
‖a⁻¹‖ = ‖a‖
source
@[simp]
theorem norm_neg {E : Type u_6} [seminormed_add_group E] (a : E) :
‖-a‖ = ‖a‖
source
@[simp]
theorem dist_mul_self_right {E : Type u_6} [seminormed_group E] (a b : E) :
has_dist.dist b (a * b) = ‖a‖
source
@[simp]
theorem dist_add_self_right {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist b (a + b) = ‖a‖
source
@[simp]
theorem dist_add_self_left {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist (a + b) b = ‖a‖
source
@[simp]
theorem dist_mul_self_left {E : Type u_6} [seminormed_group E] (a b : E) :
has_dist.dist (a * b) b = ‖a‖
source
@[simp]
theorem dist_div_eq_dist_mul_left {E : Type u_6} [seminormed_group E] (a b c : E) :
has_dist.dist (a / b) c = has_dist.dist a (c * b)
source
@[simp]
theorem dist_sub_eq_dist_add_left {E : Type u_6} [seminormed_add_group E] (a b c : E) :
has_dist.dist (a - b) c = has_dist.dist a (c + b)
source
@[simp]
theorem dist_sub_eq_dist_add_right {E : Type u_6} [seminormed_add_group E] (a b c : E) :
has_dist.dist a (b - c) = has_dist.dist (a + c) b
source
@[simp]
theorem dist_div_eq_dist_mul_right {E : Type u_6} [seminormed_group E] (a b c : E) :
has_dist.dist a (b / c) = has_dist.dist (a * c) b
source
theorem filter.tendsto_inv_cobounded {E : Type u_6} [seminormed_group E] :
filter.tendsto has_inv.inv (filter.comap has_norm.norm filter.at_top) (filter.comap has_norm.norm filter.at_top)

In a (semi)normed group, inversion x ↦ x⁻¹ tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

source
theorem filter.tendsto_neg_cobounded {E : Type u_6} [seminormed_add_group E] :
filter.tendsto has_neg.neg (filter.comap has_norm.norm filter.at_top) (filter.comap has_norm.norm filter.at_top)

In a (semi)normed group, negation x ↦ -x tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

source
theorem norm_add_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a + b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

source
theorem norm_mul_le' {E : Type u_6} [seminormed_group E] (a b : E) :
‖a * b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

source
theorem norm_mul_le_of_le {E : Type u_6} [seminormed_group E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) :
‖a₁ * a₂‖ ≤ r₁ + r₂
source
theorem norm_add_le_of_le {E : Type u_6} [seminormed_add_group E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) :
‖a₁ + a₂‖ ≤ r₁ + r₂
source
theorem norm_add₃_le {E : Type u_6} [seminormed_add_group E] (a b c : E) :
‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
source
theorem norm_mul₃_le {E : Type u_6} [seminormed_group E] (a b c : E) :
‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
source
@[simp]
theorem norm_nonneg {E : Type u_6} [seminormed_add_group E] (a : E) :
0 ≤ ‖a‖
source
@[simp]
theorem norm_nonneg' {E : Type u_6} [seminormed_group E] (a : E) :
0 ≤ ‖a‖
source
meta def tactic.positivity_norm  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: norms are nonnegative.

source
@[simp]
theorem norm_zero {E : Type u_6} [seminormed_add_group E] :
‖0‖ = 0
source
@[simp]
theorem norm_one' {E : Type u_6} [seminormed_group E] :
‖1‖ = 0
source
theorem ne_zero_of_norm_ne_zero {E : Type u_6} [seminormed_add_group E] {a : E} :
‖a‖ ≠ 0 → a ≠ 0
source
theorem ne_one_of_norm_ne_zero {E : Type u_6} [seminormed_group E] {a : E} :
‖a‖ ≠ 0 → a ≠ 1
source
theorem norm_of_subsingleton {E : Type u_6} [seminormed_add_group E] [subsingleton E] (a : E) :
‖a‖ = 0
source
theorem norm_of_subsingleton' {E : Type u_6} [seminormed_group E] [subsingleton E] (a : E) :
‖a‖ = 0
source
theorem zero_lt_one_add_norm_sq {E : Type u_6} [seminormed_add_group E] (x : E) :
0 < 1 + ‖x‖ ^ 2
source
theorem zero_lt_one_add_norm_sq' {E : Type u_6} [seminormed_group E] (x : E) :
0 < 1 + ‖x‖ ^ 2
source
theorem norm_sub_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a - b‖ ≤ ‖a‖ + ‖b‖
source
theorem norm_div_le {E : Type u_6} [seminormed_group E] (a b : E) :
‖a / b‖ ≤ ‖a‖ + ‖b‖
source
theorem norm_div_le_of_le {E : Type u_6} [seminormed_group E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) :
‖a₁ / a₂‖ ≤ r₁ + r₂
source
theorem norm_sub_le_of_le {E : Type u_6} [seminormed_add_group E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) :
‖a₁ - a₂‖ ≤ r₁ + r₂
source
theorem dist_le_norm_add_norm' {E : Type u_6} [seminormed_group E] (a b : E) :
has_dist.dist a b ≤ ‖a‖ + ‖b‖
source
theorem dist_le_norm_add_norm {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist a b ≤ ‖a‖ + ‖b‖
source
theorem abs_norm_sub_norm_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
|‖a‖ - ‖b‖| ≤ ‖a - b‖
source
theorem abs_norm_sub_norm_le' {E : Type u_6} [seminormed_group E] (a b : E) :
|‖a‖ - ‖b‖| ≤ ‖a / b‖
source
theorem norm_sub_norm_le' {E : Type u_6} [seminormed_group E] (a b : E) :
‖a‖ - ‖b‖ ≤ ‖a / b‖
source
theorem norm_sub_norm_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a‖ - ‖b‖ ≤ ‖a - b‖
source
theorem dist_norm_norm_le' {E : Type u_6} [seminormed_group E] (a b : E) :
has_dist.dist ‖a‖ ‖b‖ ≤ ‖a / b‖
source
theorem dist_norm_norm_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_dist.dist ‖a‖ ‖b‖ ≤ ‖a - b‖
source
theorem norm_le_norm_add_norm_div' {E : Type u_6} [seminormed_group E] (u v : E) :
‖u‖ ≤ ‖v‖ + ‖u / v‖
source
theorem norm_le_norm_add_norm_sub' {E : Type u_6} [seminormed_add_group E] (u v : E) :
‖u‖ ≤ ‖v‖ + ‖u - v‖
source
theorem norm_le_norm_add_norm_div {E : Type u_6} [seminormed_group E] (u v : E) :
‖v‖ ≤ ‖u‖ + ‖u / v‖
source
theorem norm_le_norm_add_norm_sub {E : Type u_6} [seminormed_add_group E] (u v : E) :
‖v‖ ≤ ‖u‖ + ‖u - v‖
source
theorem norm_le_insert' {E : Type u_6} [seminormed_add_group E] (u v : E) :
‖u‖ ≤ ‖v‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub'.

source
theorem norm_le_insert {E : Type u_6} [seminormed_add_group E] (u v : E) :
‖v‖ ≤ ‖u‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub.

source
theorem norm_le_add_norm_add {E : Type u_6} [seminormed_add_group E] (u v : E) :
‖u‖ ≤ ‖u + v‖ + ‖v‖
source
theorem norm_le_mul_norm_add {E : Type u_6} [seminormed_group E] (u v : E) :
‖u‖ ≤ ‖u * v‖ + ‖v‖
source
theorem ball_eq {E : Type u_6} [seminormed_add_group E] (y : E) (ε : ℝ) :
metric.ball y ε = {x : E | ‖x - y‖ < ε}
source
theorem ball_eq' {E : Type u_6} [seminormed_group E] (y : E) (ε : ℝ) :
metric.ball y ε = {x : E | ‖x / y‖ < ε}
source
theorem ball_zero_eq {E : Type u_6} [seminormed_add_group E] (r : ℝ) :
metric.ball 0 r = {x : E | ‖x‖ < r}
source
theorem ball_one_eq {E : Type u_6} [seminormed_group E] (r : ℝ) :
metric.ball 1 r = {x : E | ‖x‖ < r}
source
theorem mem_ball_iff_norm'' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} :
b ∈ metric.ball a r ↔ ‖b / a‖ < r
source
theorem mem_ball_iff_norm {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} :
b ∈ metric.ball a r ↔ ‖b - a‖ < r
source
theorem mem_ball_iff_norm' {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} :
b ∈ metric.ball a r ↔ ‖a - b‖ < r
source
theorem mem_ball_iff_norm''' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} :
b ∈ metric.ball a r ↔ ‖a / b‖ < r
source
@[simp]
theorem mem_ball_zero_iff {E : Type u_6} [seminormed_add_group E] {a : E} {r : ℝ} :
a ∈ metric.ball 0 r ↔ ‖a‖ < r
source
@[simp]
theorem mem_ball_one_iff {E : Type u_6} [seminormed_group E] {a : E} {r : ℝ} :
a ∈ metric.ball 1 r ↔ ‖a‖ < r
source
theorem mem_closed_ball_iff_norm'' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} :
b ∈ metric.closed_ball a r ↔ ‖b / a‖ ≤ r
source
theorem mem_closed_ball_iff_norm {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} :
b ∈ metric.closed_ball a r ↔ ‖b - a‖ ≤ r
source
@[simp]
theorem mem_closed_ball_one_iff {E : Type u_6} [seminormed_group E] {a : E} {r : ℝ} :
a ∈ metric.closed_ball 1 r ↔ ‖a‖ ≤ r
source
@[simp]
theorem mem_closed_ball_zero_iff {E : Type u_6} [seminormed_add_group E] {a : E} {r : ℝ} :
a ∈ metric.closed_ball 0 r ↔ ‖a‖ ≤ r
source
theorem mem_closed_ball_iff_norm''' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} :
b ∈ metric.closed_ball a r ↔ ‖a / b‖ ≤ r
source
theorem mem_closed_ball_iff_norm' {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} :
b ∈ metric.closed_ball a r ↔ ‖a - b‖ ≤ r
source
theorem norm_le_of_mem_closed_ball' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} (h : b ∈ metric.closed_ball a r) :
‖b‖ ≤ ‖a‖ + r
source
theorem norm_le_of_mem_closed_ball {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} (h : b ∈ metric.closed_ball a r) :
‖b‖ ≤ ‖a‖ + r
source
theorem norm_le_norm_add_const_of_dist_le {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} :
has_dist.dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r
source
theorem norm_le_norm_add_const_of_dist_le' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} :
has_dist.dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r
source
theorem norm_lt_of_mem_ball {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} (h : b ∈ metric.ball a r) :
‖b‖ < ‖a‖ + r
source
theorem norm_lt_of_mem_ball' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} (h : b ∈ metric.ball a r) :
‖b‖ < ‖a‖ + r
source
theorem norm_div_sub_norm_div_le_norm_div {E : Type u_6} [seminormed_group E] (u v w : E) :
‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖
source
theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_6} [seminormed_add_group E] (u v w : E) :
‖u - w‖ - ‖v - w‖ ≤ ‖u - v‖
source
theorem bounded_iff_forall_norm_le' {E : Type u_6} [seminormed_group E] {s : set E} :
metric.bounded s ↔ ∃ (C : ℝ), ∀ (x : E), x ∈ s → ‖x‖ ≤ C
source
theorem bounded_iff_forall_norm_le {E : Type u_6} [seminormed_add_group E] {s : set E} :
metric.bounded s ↔ ∃ (C : ℝ), ∀ (x : E), x ∈ s → ‖x‖ ≤ C
source
theorem metric.bounded.exists_norm_le' {E : Type u_6} [seminormed_group E] {s : set E} :
metric.bounded s → (∃ (C : ℝ), ∀ (x : E), x ∈ s → ‖x‖ ≤ C)

Alias of the forward direction of bounded_iff_forall_norm_le'.

source
theorem metric.bounded.exists_norm_le {E : Type u_6} [seminormed_add_group E] {s : set E} :
metric.bounded s → (∃ (C : ℝ), ∀ (x : E), x ∈ s → ‖x‖ ≤ C)

Alias of the forward direction of bounded_iff_forall_norm_le.

source
theorem metric.bounded.exists_pos_norm_le {E : Type u_6} [seminormed_add_group E] {s : set E} (hs : metric.bounded s) :
∃ (R : ℝ) (H : R > 0), ∀ (x : E), x ∈ s → ‖x‖ ≤ R
source
theorem metric.bounded.exists_pos_norm_le' {E : Type u_6} [seminormed_group E] {s : set E} (hs : metric.bounded s) :
∃ (R : ℝ) (H : R > 0), ∀ (x : E), x ∈ s → ‖x‖ ≤ R
source
@[simp]
theorem mem_sphere_iff_norm {E : Type u_6} [seminormed_add_group E] {a b : E} {r : ℝ} :
b ∈ metric.sphere a r ↔ ‖b - a‖ = r
source
@[simp]
theorem mem_sphere_iff_norm' {E : Type u_6} [seminormed_group E] {a b : E} {r : ℝ} :
b ∈ metric.sphere a r ↔ ‖b / a‖ = r
source
@[simp]
theorem mem_sphere_one_iff_norm {E : Type u_6} [seminormed_group E] {a : E} {r : ℝ} :
a ∈ metric.sphere 1 r ↔ ‖a‖ = r
source
@[simp]
theorem mem_sphere_zero_iff_norm {E : Type u_6} [seminormed_add_group E] {a : E} {r : ℝ} :
a ∈ metric.sphere 0 r ↔ ‖a‖ = r
source
@[simp]
theorem norm_eq_of_mem_sphere' {E : Type u_6} [seminormed_group E] {r : ℝ} (x : ↥(metric.sphere 1 r)) :
‖↑x‖ = r
source
@[simp]
theorem norm_eq_of_mem_sphere {E : Type u_6} [seminormed_add_group E] {r : ℝ} (x : ↥(metric.sphere 0 r)) :
‖↑x‖ = r
source
theorem ne_zero_of_mem_sphere {E : Type u_6} [seminormed_add_group E] {r : ℝ} (hr : r ≠ 0) (x : ↥(metric.sphere 0 r)) :
↑x ≠ 0
source
theorem ne_one_of_mem_sphere {E : Type u_6} [seminormed_group E] {r : ℝ} (hr : r ≠ 0) (x : ↥(metric.sphere 1 r)) :
↑x ≠ 1
source
theorem ne_one_of_mem_unit_sphere {E : Type u_6} [seminormed_group E] (x : ↥(metric.sphere 1 1)) :
↑x ≠ 1
source
theorem ne_zero_of_mem_unit_sphere {E : Type u_6} [seminormed_add_group E] (x : ↥(metric.sphere 0 1)) :
↑x ≠ 0
source
def norm_group_seminorm (E : Type u_6) [seminormed_group E] :
group_seminorm E

The norm of a seminormed group as a group seminorm.

Equations
source
def norm_add_group_seminorm (E : Type u_6) [seminormed_add_group E] :
add_group_seminorm E

The norm of a seminormed group as an additive group seminorm.

Equations
source
@[simp]
theorem coe_norm_add_group_seminorm (E : Type u_6) [seminormed_add_group E] :
⇑(norm_add_group_seminorm E) = has_norm.norm
source
@[simp]
theorem coe_norm_group_seminorm (E : Type u_6) [seminormed_group E] :
⇑(norm_group_seminorm E) = has_norm.norm
source
theorem normed_comm_group.tendsto_nhds_one {α : Type u_3} {E : Type u_6} [seminormed_group E] {f : α → E} {l : filter α} :
filter.tendsto f l (nhds 1) ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : α) in l, ‖f x‖ < ε)
source
theorem normed_add_comm_group.tendsto_nhds_zero {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {f : α → E} {l : filter α} :
filter.tendsto f l (nhds 0) ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : α) in l, ‖f x‖ < ε)
source
theorem normed_comm_group.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {x : E} {y : F} :
filter.tendsto f (nhds x) (nhds y) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε)
source
theorem normed_add_comm_group.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {x : E} {y : F} :
filter.tendsto f (nhds x) (nhds y) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x' : E), ‖x' - x‖ < δ → ‖f x' - y‖ < ε)
source
theorem normed_add_comm_group.cauchy_seq_iff {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [nonempty α] [semilattice_sup α] {u : α → E} :
cauchy_seq u ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m - u n‖ < ε)
source
theorem normed_comm_group.cauchy_seq_iff {α : Type u_3} {E : Type u_6} [seminormed_group E] [nonempty α] [semilattice_sup α] {u : α → E} :
cauchy_seq u ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε)
source
theorem normed_comm_group.nhds_basis_norm_lt {E : Type u_6} [seminormed_group E] (x : E) :
(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ‖y / x‖ < ε})
source
theorem normed_add_comm_group.nhds_basis_norm_lt {E : Type u_6} [seminormed_add_group E] (x : E) :
(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ‖y - x‖ < ε})
source
theorem normed_comm_group.nhds_one_basis_norm_lt {E : Type u_6} [seminormed_group E] :
(nhds 1).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ‖y‖ < ε})
source
theorem normed_add_comm_group.nhds_zero_basis_norm_lt {E : Type u_6} [seminormed_add_group E] :
(nhds 0).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ‖y‖ < ε})
source
theorem normed_comm_group.uniformity_basis_dist {E : Type u_6} [seminormed_group E] :
(uniformity E).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : E × E | ‖p.fst / p.snd‖ < ε})
source
theorem normed_add_comm_group.uniformity_basis_dist {E : Type u_6} [seminormed_add_group E] :
(uniformity E).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : E × E | ‖p.fst - p.snd‖ < ε})
source
theorem monoid_hom_class.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :
lipschitz_with C.to_nnreal ⇑f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in normed_space.operator_norm.

source
theorem add_monoid_hom_class.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :
lipschitz_with C.to_nnreal ⇑f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in normed_space.operator_norm.

source
theorem lipschitz_on_with_iff_norm_div_le {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {s : set E} {f : E → F} {C : nnreal} :
lipschitz_on_with C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
source
theorem lipschitz_on_with_iff_norm_sub_le {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {s : set E} {f : E → F} {C : nnreal} :
lipschitz_on_with C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
source
theorem lipschitz_on_with.norm_div_le {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {s : set E} {f : E → F} {C : nnreal} :
lipschitz_on_with C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitz_on_with_iff_norm_div_le.

source
theorem lipschitz_on_with.norm_sub_le {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {s : set E} {f : E → F} {C : nnreal} :
lipschitz_on_with C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

Alias of the forward direction of lipschitz_on_with_iff_norm_div_le.

source
theorem lipschitz_on_with.norm_sub_le_of_le {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {s : set E} {a b : E} {r : ℝ} {f : E → F} {C : nnreal} (h : lipschitz_on_with C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a - b‖ ≤ r) :
‖f a - f b‖ ≤ ↑C * r
source
theorem lipschitz_on_with.norm_div_le_of_le {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {s : set E} {a b : E} {r : ℝ} {f : E → F} {C : nnreal} (h : lipschitz_on_with C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) :
‖f a / f b‖ ≤ ↑C * r
source
theorem lipschitz_with_iff_norm_sub_le {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {C : nnreal} :
lipschitz_with C f ↔ ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖
source
theorem lipschitz_with_iff_norm_div_le {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {C : nnreal} :
lipschitz_with C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖
source
theorem lipschitz_with.norm_div_le {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {C : nnreal} :
lipschitz_with C f → ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitz_with_iff_norm_div_le.

source
theorem lipschitz_with.norm_sub_le {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {C : nnreal} :
lipschitz_with C f → ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

Alias of the forward direction of lipschitz_with_iff_norm_div_le.

source
theorem lipschitz_with.norm_div_le_of_le {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {a b : E} {r : ℝ} {f : E → F} {C : nnreal} (h : lipschitz_with C f) (hr : ‖a / b‖ ≤ r) :
‖f a / f b‖ ≤ ↑C * r
source
theorem lipschitz_with.norm_sub_le_of_le {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {a b : E} {r : ℝ} {f : E → F} {C : nnreal} (h : lipschitz_with C f) (hr : ‖a - b‖ ≤ r) :
‖f a - f b‖ ≤ ↑C * r
source
theorem monoid_hom_class.continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :
continuous ⇑f

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖.

source
theorem add_monoid_hom_class.continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :
continuous ⇑f

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖

source
theorem add_monoid_hom_class.uniform_continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :
uniform_continuous ⇑f
source
theorem monoid_hom_class.uniform_continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :
uniform_continuous ⇑f
source
theorem is_compact.exists_bound_of_continuous_on' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {s : set α} (hs : is_compact s) {f : α → E} (hf : continuous_on f s) :
∃ (C : ℝ), ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
source
theorem is_compact.exists_bound_of_continuous_on {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {s : set α} (hs : is_compact s) {f : α → E} (hf : continuous_on f s) :
∃ (C : ℝ), ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
source
theorem monoid_hom_class.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) :
isometry ⇑f ↔ ∀ (x : E), ‖⇑f x‖ = ‖x‖
source
theorem add_monoid_hom_class.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) :
isometry ⇑f ↔ ∀ (x : E), ‖⇑f x‖ = ‖x‖
source
theorem monoid_hom_class.isometry_of_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) :
(∀ (x : E), ‖⇑f x‖ = ‖x‖) → isometry ⇑f

Alias of the reverse direction of monoid_hom_class.isometry_iff_norm.

source
theorem add_monoid_hom_class.isometry_of_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) :
(∀ (x : E), ‖⇑f x‖ = ‖x‖) → isometry ⇑f

Alias of the reverse direction of monoid_hom_class.isometry_iff_norm.

source
@[protected, instance]
def seminormed_group.to_has_nnnorm {E : Type u_6} [seminormed_group E] :
has_nnnorm E
Equations
source
@[protected, instance]
def seminormed_add_group.to_has_nnnorm {E : Type u_6} [seminormed_add_group E] :
has_nnnorm E
Equations
source
@[simp, norm_cast]
theorem coe_nnnorm' {E : Type u_6} [seminormed_group E] (a : E) :
↑‖a‖₊ = ‖a‖
source
@[simp, norm_cast]
theorem coe_nnnorm {E : Type u_6} [seminormed_add_group E] (a : E) :
↑‖a‖₊ = ‖a‖
source
@[simp]
theorem coe_comp_nnnorm {E : Type u_6} [seminormed_add_group E] :
coe ∘ has_nnnorm.nnnorm = has_norm.norm
source
@[simp]
theorem coe_comp_nnnorm' {E : Type u_6} [seminormed_group E] :
coe ∘ has_nnnorm.nnnorm = has_norm.norm
source
theorem norm_to_nnreal {E : Type u_6} [seminormed_add_group E] {a : E} :
‖a‖.to_nnreal = ‖a‖₊
source
theorem norm_to_nnreal' {E : Type u_6} [seminormed_group E] {a : E} :
‖a‖.to_nnreal = ‖a‖₊
source
theorem nndist_eq_nnnorm_div {E : Type u_6} [seminormed_group E] (a b : E) :
has_nndist.nndist a b = ‖a / b‖₊
source
theorem nndist_eq_nnnorm_sub {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_nndist.nndist a b = ‖a - b‖₊
source
theorem nndist_eq_nnnorm {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_nndist.nndist a b = ‖a - b‖₊

Alias of nndist_eq_nnnorm_sub.

source
@[simp]
theorem nnnorm_zero {E : Type u_6} [seminormed_add_group E] :
‖0‖₊ = 0
source
@[simp]
theorem nnnorm_one' {E : Type u_6} [seminormed_group E] :
‖1‖₊ = 0
source
theorem ne_one_of_nnnorm_ne_zero {E : Type u_6} [seminormed_group E] {a : E} :
‖a‖₊ ≠ 0 → a ≠ 1
source
theorem ne_zero_of_nnnorm_ne_zero {E : Type u_6} [seminormed_add_group E] {a : E} :
‖a‖₊ ≠ 0 → a ≠ 0
source
theorem nnnorm_mul_le' {E : Type u_6} [seminormed_group E] (a b : E) :
‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊
source
theorem nnnorm_add_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊
source
@[simp]
theorem nnnorm_inv' {E : Type u_6} [seminormed_group E] (a : E) :
‖a⁻¹‖₊ = ‖a‖₊
source
@[simp]
theorem nnnorm_neg {E : Type u_6} [seminormed_add_group E] (a : E) :
‖-a‖₊ = ‖a‖₊
source
theorem nnnorm_sub_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊
source
theorem nnnorm_div_le {E : Type u_6} [seminormed_group E] (a b : E) :
‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊
source
theorem nndist_nnnorm_nnnorm_le' {E : Type u_6} [seminormed_group E] (a b : E) :
has_nndist.nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊
source
theorem nndist_nnnorm_nnnorm_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_nndist.nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊
source
theorem nnnorm_le_nnnorm_add_nnnorm_sub {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊
source
theorem nnnorm_le_nnnorm_add_nnnorm_div {E : Type u_6} [seminormed_group E] (a b : E) :
‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊
source
theorem nnnorm_le_nnnorm_add_nnnorm_sub' {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊
source
theorem nnnorm_le_nnnorm_add_nnnorm_div' {E : Type u_6} [seminormed_group E] (a b : E) :
‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊
source
theorem nnnorm_le_insert' {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊

Alias of nnnorm_le_nnnorm_add_nnnorm_sub'.

source
theorem nnnorm_le_insert {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊

Alias of nnnorm_le_nnnorm_add_nnnorm_sub.

source
theorem nnnorm_le_mul_nnnorm_add {E : Type u_6} [seminormed_group E] (a b : E) :
‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊
source
theorem nnnorm_le_add_nnnorm_add {E : Type u_6} [seminormed_add_group E] (a b : E) :
‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊
source
theorem of_real_norm_eq_coe_nnnorm {E : Type u_6} [seminormed_add_group E] (a : E) :
ennreal.of_real ‖a‖ = ↑‖a‖₊
source
theorem of_real_norm_eq_coe_nnnorm' {E : Type u_6} [seminormed_group E] (a : E) :
ennreal.of_real ‖a‖ = ↑‖a‖₊
source
theorem edist_eq_coe_nnnorm_sub {E : Type u_6} [seminormed_add_group E] (a b : E) :
has_edist.edist a b = ↑‖a - b‖₊
source
theorem edist_eq_coe_nnnorm_div {E : Type u_6} [seminormed_group E] (a b : E) :
has_edist.edist a b = ↑‖a / b‖₊
source
theorem edist_eq_coe_nnnorm' {E : Type u_6} [seminormed_group E] (x : E) :
has_edist.edist x 1 = ↑‖x‖₊
source
theorem edist_eq_coe_nnnorm {E : Type u_6} [seminormed_add_group E] (x : E) :
has_edist.edist x 0 = ↑‖x‖₊
source
theorem mem_emetric_ball_one_iff {E : Type u_6} [seminormed_group E] {a : E} {r : ennreal} :
a ∈ emetric.ball 1 r ↔ ↑‖a‖₊ < r
source
theorem mem_emetric_ball_zero_iff {E : Type u_6} [seminormed_add_group E] {a : E} {r : ennreal} :
a ∈ emetric.ball 0 r ↔ ↑‖a‖₊ < r
source
theorem monoid_hom_class.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) (C : nnreal) (h : ∀ (x : E), ‖⇑f x‖₊ ≤ C * ‖x‖₊) :
lipschitz_with C ⇑f
source
theorem add_monoid_hom_class.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (C : nnreal) (h : ∀ (x : E), ‖⇑f x‖₊ ≤ C * ‖x‖₊) :
lipschitz_with C ⇑f
source
theorem monoid_hom_class.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) {K : nnreal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖⇑f x‖) :
antilipschitz_with K ⇑f
source
theorem add_monoid_hom_class.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) {K : nnreal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖⇑f x‖) :
antilipschitz_with K ⇑f
source
theorem lipschitz_with.norm_le_mul' {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {K : nnreal} (h : lipschitz_with K f) (hf : f 1 = 1) (x : E) :
‖f x‖ ≤ ↑K * ‖x‖
source
theorem lipschitz_with.norm_le_mul {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {K : nnreal} (h : lipschitz_with K f) (hf : f 0 = 0) (x : E) :
‖f x‖ ≤ ↑K * ‖x‖
source
theorem lipschitz_with.nnorm_le_mul' {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {K : nnreal} (h : lipschitz_with K f) (hf : f 1 = 1) (x : E) :
‖f x‖₊ ≤ K * ‖x‖₊
source
theorem lipschitz_with.nnorm_le_mul {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {K : nnreal} (h : lipschitz_with K f) (hf : f 0 = 0) (x : E) :
‖f x‖₊ ≤ K * ‖x‖₊
source
theorem antilipschitz_with.le_mul_norm' {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {K : nnreal} (h : antilipschitz_with K f) (hf : f 1 = 1) (x : E) :
‖x‖ ≤ ↑K * ‖f x‖
source
theorem antilipschitz_with.le_mul_norm {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {K : nnreal} (h : antilipschitz_with K f) (hf : f 0 = 0) (x : E) :
‖x‖ ≤ ↑K * ‖f x‖
source
theorem antilipschitz_with.le_mul_nnnorm' {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] {f : E → F} {K : nnreal} (h : antilipschitz_with K f) (hf : f 1 = 1) (x : E) :
‖x‖₊ ≤ K * ‖f x‖₊
source
theorem antilipschitz_with.le_mul_nnnorm {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] {f : E → F} {K : nnreal} (h : antilipschitz_with K f) (hf : f 0 = 0) (x : E) :
‖x‖₊ ≤ K * ‖f x‖₊
source
theorem one_hom_class.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] [one_hom_class 𝓕 E F] (f : 𝓕) {K : nnreal} (h : antilipschitz_with K ⇑f) (x : E) :
‖x‖ ≤ ↑K * ‖⇑f x‖
source
theorem zero_hom_class.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] [zero_hom_class 𝓕 E F] (f : 𝓕) {K : nnreal} (h : antilipschitz_with K ⇑f) (x : E) :
‖x‖ ≤ ↑K * ‖⇑f x‖
source
theorem tendsto_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {f : α → E} {a : filter α} {b : E} :
filter.tendsto f a (nhds b) ↔ filter.tendsto (λ (e : α), ‖f e - b‖) a (nhds 0)
source
theorem tendsto_iff_norm_tendsto_one {α : Type u_3} {E : Type u_6} [seminormed_group E] {f : α → E} {a : filter α} {b : E} :
filter.tendsto f a (nhds b) ↔ filter.tendsto (λ (e : α), ‖f e / b‖) a (nhds 0)
source
theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {f : α → E} {a : filter α} :
filter.tendsto f a (nhds 0) ↔ filter.tendsto (λ (e : α), ‖f e‖) a (nhds 0)
source
theorem tendsto_one_iff_norm_tendsto_one {α : Type u_3} {E : Type u_6} [seminormed_group E] {f : α → E} {a : filter α} :
filter.tendsto f a (nhds 1) ↔ filter.tendsto (λ (e : α), ‖f e‖) a (nhds 0)
source
theorem comap_norm_nhds_zero {E : Type u_6} [seminormed_add_group E] :
filter.comap has_norm.norm (nhds 0) = nhds 0
source
theorem comap_norm_nhds_one {E : Type u_6} [seminormed_group E] :
filter.comap has_norm.norm (nhds 0) = nhds 1
source
theorem squeeze_one_norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] {f : α → E} {a : α → ℝ} {t₀ : filter α} (h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) (h' : filter.tendsto a t₀ (nhds 0)) :
filter.tendsto f t₀ (nhds 1)

Special case of the sandwich theorem: if the norm of f is eventually bounded by a real function a which tends to 0, then f tends to 1. In this pair of lemmas (squeeze_one_norm' and squeeze_one_norm), following a convention of similar lemmas in topology.metric_space.basic and topology.algebra.order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

source
theorem squeeze_zero_norm' {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {f : α → E} {a : α → ℝ} {t₀ : filter α} (h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) (h' : filter.tendsto a t₀ (nhds 0)) :
filter.tendsto f t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of f is eventually bounded by a real function a which tends to 0, then f tends to 1. In this pair of lemmas (squeeze_zero_norm' and squeeze_zero_norm), following a convention of similar lemmas in topology.metric_space.basic and topology.algebra.order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

source
theorem squeeze_zero_norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {f : α → E} {a : α → ℝ} {t₀ : filter α} (h : ∀ (n : α), ‖f n‖ ≤ a n) :
filter.tendsto a t₀ (nhds 0) → filter.tendsto f t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of f is bounded by a real function a which tends to 0, then f tends to 0.

source
theorem squeeze_one_norm {α : Type u_3} {E : Type u_6} [seminormed_group E] {f : α → E} {a : α → ℝ} {t₀ : filter α} (h : ∀ (n : α), ‖f n‖ ≤ a n) :
filter.tendsto a t₀ (nhds 0) → filter.tendsto f t₀ (nhds 1)

Special case of the sandwich theorem: if the norm of f is bounded by a real function a which tends to 0, then f tends to 1.

source
theorem tendsto_norm_div_self {E : Type u_6} [seminormed_group E] (x : E) :
filter.tendsto (λ (a : E), ‖a / x‖) (nhds x) (nhds 0)
source
theorem tendsto_norm_sub_self {E : Type u_6} [seminormed_add_group E] (x : E) :
filter.tendsto (λ (a : E), ‖a - x‖) (nhds x) (nhds 0)
source
theorem tendsto_norm {E : Type u_6} [seminormed_add_group E] {x : E} :
filter.tendsto (λ (a : E), ‖a‖) (nhds x) (nhds ‖x‖)
source
theorem tendsto_norm' {E : Type u_6} [seminormed_group E] {x : E} :
filter.tendsto (λ (a : E), ‖a‖) (nhds x) (nhds ‖x‖)
source
theorem tendsto_norm_one {E : Type u_6} [seminormed_group E] :
filter.tendsto (λ (a : E), ‖a‖) (nhds 1) (nhds 0)
source
theorem tendsto_norm_zero {E : Type u_6} [seminormed_add_group E] :
filter.tendsto (λ (a : E), ‖a‖) (nhds 0) (nhds 0)
source
@[continuity]
theorem continuous_norm' {E : Type u_6} [seminormed_group E] :
continuous (λ (a : E), ‖a‖)
source
@[continuity]
theorem continuous_norm {E : Type u_6} [seminormed_add_group E] :
continuous (λ (a : E), ‖a‖)
source
@[continuity]
theorem continuous_nnnorm' {E : Type u_6} [seminormed_group E] :
continuous (λ (a : E), ‖a‖₊)
source
@[continuity]
theorem continuous_nnnorm {E : Type u_6} [seminormed_add_group E] :
continuous (λ (a : E), ‖a‖₊)
source
theorem lipschitz_with_one_norm {E : Type u_6} [seminormed_add_group E] :
lipschitz_with 1 has_norm.norm
source
theorem lipschitz_with_one_norm' {E : Type u_6} [seminormed_group E] :
lipschitz_with 1 has_norm.norm
source
theorem lipschitz_with_one_nnnorm {E : Type u_6} [seminormed_add_group E] :
lipschitz_with 1 has_nnnorm.nnnorm
source
theorem lipschitz_with_one_nnnorm' {E : Type u_6} [seminormed_group E] :
lipschitz_with 1 has_nnnorm.nnnorm
source
theorem uniform_continuous_norm {E : Type u_6} [seminormed_add_group E] :
uniform_continuous has_norm.norm
source
theorem uniform_continuous_norm' {E : Type u_6} [seminormed_group E] :
uniform_continuous has_norm.norm
source
theorem uniform_continuous_nnnorm' {E : Type u_6} [seminormed_group E] :
uniform_continuous (λ (a : E), ‖a‖₊)
source
theorem uniform_continuous_nnnorm {E : Type u_6} [seminormed_add_group E] :
uniform_continuous (λ (a : E), ‖a‖₊)
source
theorem mem_closure_one_iff_norm {E : Type u_6} [seminormed_group E] {x : E} :
x ∈ closure {1} ↔ ‖x‖ = 0
source
theorem mem_closure_zero_iff_norm {E : Type u_6} [seminormed_add_group E] {x : E} :
x ∈ closure {0} ↔ ‖x‖ = 0
source
theorem closure_one_eq {E : Type u_6} [seminormed_group E] :
closure {1} = {x : E | ‖x‖ = 0}
source
theorem closure_zero_eq {E : Type u_6} [seminormed_add_group E] :
closure {0} = {x : E | ‖x‖ = 0}
source
theorem filter.tendsto.op_zero_is_bounded_under_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [seminormed_add_group E] [seminormed_add_group F] [seminormed_add_group G] {f : α → E} {g : α → F} {l : filter α} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

source
theorem filter.tendsto.op_one_is_bounded_under_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [seminormed_group E] [seminormed_group F] [seminormed_group G] {f : α → E} {g : α → F} {l : filter α} (hf : filter.tendsto f l (nhds 1)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

source
theorem filter.tendsto.op_one_is_bounded_under_le {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [seminormed_group E] [seminormed_group F] [seminormed_group G] {f : α → E} {g : α → F} {l : filter α} (hf : filter.tendsto f l (nhds 1)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

source
theorem filter.tendsto.op_zero_is_bounded_under_le {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [seminormed_add_group E] [seminormed_add_group F] [seminormed_add_group G] {f : α → E} {g : α → F} {l : filter α} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

source
theorem filter.tendsto.norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] {a : E} {l : filter α} {f : α → E} (h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (x : α), ‖f x‖) l (nhds ‖a‖)
source
theorem filter.tendsto.norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {a : E} {l : filter α} {f : α → E} (h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (x : α), ‖f x‖) l (nhds ‖a‖)
source
theorem filter.tendsto.nnnorm' {α : Type u_3} {E : Type u_6} [seminormed_group E] {a : E} {l : filter α} {f : α → E} (h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (x : α), ‖f x‖₊) l (nhds ‖a‖₊)
source
theorem filter.tendsto.nnnorm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {a : E} {l : filter α} {f : α → E} (h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (x : α), ‖f x‖₊) l (nhds ‖a‖₊)
source
theorem continuous.norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} :
continuous f → continuous (λ (x : α), ‖f x‖)
source
theorem continuous.norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} :
continuous f → continuous (λ (x : α), ‖f x‖)
source
theorem continuous.nnnorm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} :
continuous f → continuous (λ (x : α), ‖f x‖₊)
source
theorem continuous.nnnorm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} :
continuous f → continuous (λ (x : α), ‖f x‖₊)
source
theorem continuous_at.norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), ‖f x‖) a
source
theorem continuous_at.norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), ‖f x‖) a
source
theorem continuous_at.nnnorm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), ‖f x‖₊) a
source
theorem continuous_at.nnnorm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), ‖f x‖₊) a
source
theorem continuous_within_at.norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ‖f x‖) s a
source
theorem continuous_within_at.norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ‖f x‖) s a
source
theorem continuous_within_at.nnnorm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ‖f x‖₊) s a
source
theorem continuous_within_at.nnnorm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ‖f x‖₊) s a
source
theorem continuous_on.norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), ‖f x‖) s
source
theorem continuous_on.norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), ‖f x‖) s
source
theorem continuous_on.nnnorm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), ‖f x‖₊) s
source
theorem continuous_on.nnnorm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), ‖f x‖₊) s
source
theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_3} {E : Type u_6} [seminormed_add_group E] {l : filter α} {f : α → E} (h : filter.tendsto (λ (y : α), ‖f y‖) l filter.at_top) (x : E) :
∀ᶠ (y : α) in l, f y ≠ x

If ‖y‖→∞, then we can assume y≠x for any fixed x

source
theorem eventually_ne_of_tendsto_norm_at_top' {α : Type u_3} {E : Type u_6} [seminormed_group E] {l : filter α} {f : α → E} (h : filter.tendsto (λ (y : α), ‖f y‖) l filter.at_top) (x : E) :
∀ᶠ (y : α) in l, f y ≠ x

If ‖y‖ → ∞, then we can assume y ≠ x for any fixed x.

source
theorem seminormed_add_comm_group.mem_closure_iff {E : Type u_6} [seminormed_add_group E] {s : set E} {a : E} :
a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → (∃ (b : E) (H : b ∈ s), ‖a - b‖ < ε)
source
theorem seminormed_comm_group.mem_closure_iff {E : Type u_6} [seminormed_group E] {s : set E} {a : E} :
a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → (∃ (b : E) (H : b ∈ s), ‖a / b‖ < ε)
source
theorem norm_le_zero_iff' {E : Type u_6} [seminormed_add_group E] [t0_space E] {a : E} :
‖a‖ ≤ 0 ↔ a = 0
source
theorem norm_le_zero_iff''' {E : Type u_6} [seminormed_group E] [t0_space E] {a : E} :
‖a‖ ≤ 0 ↔ a = 1
source
theorem norm_eq_zero''' {E : Type u_6} [seminormed_group E] [t0_space E] {a : E} :
‖a‖ = 0 ↔ a = 1
source
theorem norm_eq_zero' {E : Type u_6} [seminormed_add_group E] [t0_space E] {a : E} :
‖a‖ = 0 ↔ a = 0
source
theorem norm_pos_iff' {E : Type u_6} [seminormed_add_group E] [t0_space E] {a : E} :
0 < ‖a‖ ↔ a ≠ 0
source
theorem norm_pos_iff''' {E : Type u_6} [seminormed_group E] [t0_space E] {a : E} :
0 < ‖a‖ ↔ a ≠ 1
source
theorem seminormed_add_group.tendsto_uniformly_on_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [seminormed_add_group G] {f : ι → κ → G} {s : set κ} {l : filter ι} :
tendsto_uniformly_on f 0 l s ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (i : ι) in l, ∀ (x : κ), x ∈ s → ‖f i x‖ < ε)
source
theorem seminormed_group.tendsto_uniformly_on_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [seminormed_group G] {f : ι → κ → G} {s : set κ} {l : filter ι} :
tendsto_uniformly_on f 1 l s ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (i : ι) in l, ∀ (x : κ), x ∈ s → ‖f i x‖ < ε)
source
theorem seminormed_add_group.uniform_cauchy_seq_on_filter_iff_tendsto_uniformly_on_filter_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [seminormed_add_group G] {f : ι → κ → G} {l : filter ι} {l' : filter κ} :
uniform_cauchy_seq_on_filter f l l' ↔ tendsto_uniformly_on_filter (λ (n : ι × ι) (z : κ), f n.fst z - f n.snd z) 0 (l.prod l) l'
source
theorem seminormed_group.uniform_cauchy_seq_on_filter_iff_tendsto_uniformly_on_filter_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [seminormed_group G] {f : ι → κ → G} {l : filter ι} {l' : filter κ} :
uniform_cauchy_seq_on_filter f l l' ↔ tendsto_uniformly_on_filter (λ (n : ι × ι) (z : κ), f n.fst z / f n.snd z) 1 (l.prod l) l'
source
theorem seminormed_add_group.uniform_cauchy_seq_on_iff_tendsto_uniformly_on_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [seminormed_add_group G] {f : ι → κ → G} {s : set κ} {l : filter ι} :
uniform_cauchy_seq_on f l s ↔ tendsto_uniformly_on (λ (n : ι × ι) (z : κ), f n.fst z - f n.snd z) 0 (l.prod l) s
source
theorem seminormed_group.uniform_cauchy_seq_on_iff_tendsto_uniformly_on_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [seminormed_group G] {f : ι → κ → G} {s : set κ} {l : filter ι} :
uniform_cauchy_seq_on f l s ↔ tendsto_uniformly_on (λ (n : ι × ι) (z : κ), f n.fst z / f n.snd z) 1 (l.prod l) s
source
@[reducible]
def seminormed_add_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [add_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) :
seminormed_add_group E

A group homomorphism from an add_group to a seminormed_add_group induces a seminormed_add_group structure on the domain.

Equations
source
@[reducible]
def seminormed_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) :
seminormed_group E

A group homomorphism from a group to a seminormed_group induces a seminormed_group structure on the domain.

Equations
source
@[reducible]
def seminormed_comm_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [comm_group E] [seminormed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) :
seminormed_comm_group E

A group homomorphism from a comm_group to a seminormed_group induces a seminormed_comm_group structure on the domain.

Equations
source
@[reducible]
def seminormed_add_comm_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [add_comm_group E] [seminormed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) :
seminormed_add_comm_group E

A group homomorphism from an add_comm_group to a seminormed_add_group induces a seminormed_add_comm_group structure on the domain.

Equations
source
@[reducible]
def normed_add_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [add_group E] [normed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (h : function.injective ⇑f) :
normed_add_group E

An injective group homomorphism from an add_group to a normed_add_group induces a normed_add_group structure on the domain.

Equations
source
@[reducible]
def normed_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [group E] [normed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) (h : function.injective ⇑f) :
normed_group E

An injective group homomorphism from a group to a normed_group induces a normed_group structure on the domain.

Equations
source
@[reducible]
def normed_add_comm_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [add_comm_group E] [normed_add_group F] [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (h : function.injective ⇑f) :
normed_add_comm_group E

An injective group homomorphism from an comm_group to a normed_comm_group induces a normed_comm_group structure on the domain.

Equations
source
@[reducible]
def normed_comm_group.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [comm_group E] [normed_group F] [monoid_hom_class 𝓕 E F] (f : 𝓕) (h : function.injective ⇑f) :
normed_comm_group E

An injective group homomorphism from an comm_group to a normed_group induces a normed_comm_group structure on the domain.

Equations
source
@[protected, instance]
def normed_add_group.to_has_isometric_vadd_left {E : Type u_6} [seminormed_add_comm_group E] :
has_isometric_vadd E E
source
@[protected, instance]
def normed_group.to_has_isometric_smul_left {E : Type u_6} [seminormed_comm_group E] :
has_isometric_smul E E
source
theorem dist_inv {E : Type u_6} [seminormed_comm_group E] (x y : E) :
has_dist.dist x⁻¹ y = has_dist.dist x y⁻¹
source
theorem dist_neg {E : Type u_6} [seminormed_add_comm_group E] (x y : E) :
has_dist.dist (-x) y = has_dist.dist x (-y)
source
@[simp]
theorem dist_self_add_right {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
has_dist.dist a (a + b) = ‖b‖
source
@[simp]
theorem dist_self_mul_right {E : Type u_6} [seminormed_comm_group E] (a b : E) :
has_dist.dist a (a * b) = ‖b‖
source
@[simp]
theorem dist_self_mul_left {E : Type u_6} [seminormed_comm_group E] (a b : E) :
has_dist.dist (a * b) a = ‖b‖
source
@[simp]
theorem dist_self_add_left {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
has_dist.dist (a + b) a = ‖b‖
source
@[simp]
theorem dist_self_sub_right {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
has_dist.dist a (a - b) = ‖b‖
source
@[simp]
theorem dist_self_div_right {E : Type u_6} [seminormed_comm_group E] (a b : E) :
has_dist.dist a (a / b) = ‖b‖
source
@[simp]
theorem dist_self_div_left {E : Type u_6} [seminormed_comm_group E] (a b : E) :
has_dist.dist (a / b) a = ‖b‖
source
@[simp]
theorem dist_self_sub_left {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
has_dist.dist (a - b) a = ‖b‖
source
theorem dist_add_add_le {E : Type u_6} [seminormed_add_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_dist.dist (a₁ + a₂) (b₁ + b₂) ≤ has_dist.dist a₁ b₁ + has_dist.dist a₂ b₂
source
theorem dist_mul_mul_le {E : Type u_6} [seminormed_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_dist.dist (a₁ * a₂) (b₁ * b₂) ≤ has_dist.dist a₁ b₁ + has_dist.dist a₂ b₂
source
theorem dist_mul_mul_le_of_le {E : Type u_6} [seminormed_comm_group E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : has_dist.dist a₁ b₁ ≤ r₁) (h₂ : has_dist.dist a₂ b₂ ≤ r₂) :
has_dist.dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂
source
theorem dist_add_add_le_of_le {E : Type u_6} [seminormed_add_comm_group E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : has_dist.dist a₁ b₁ ≤ r₁) (h₂ : has_dist.dist a₂ b₂ ≤ r₂) :
has_dist.dist (a₁ + a₂) (b₁ + b₂) ≤ r₁ + r₂
source
theorem dist_div_div_le {E : Type u_6} [seminormed_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_dist.dist (a₁ / a₂) (b₁ / b₂) ≤ has_dist.dist a₁ b₁ + has_dist.dist a₂ b₂
source
theorem dist_sub_sub_le {E : Type u_6} [seminormed_add_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_dist.dist (a₁ - a₂) (b₁ - b₂) ≤ has_dist.dist a₁ b₁ + has_dist.dist a₂ b₂
source
theorem dist_sub_sub_le_of_le {E : Type u_6} [seminormed_add_comm_group E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : has_dist.dist a₁ b₁ ≤ r₁) (h₂ : has_dist.dist a₂ b₂ ≤ r₂) :
has_dist.dist (a₁ - a₂) (b₁ - b₂) ≤ r₁ + r₂
source
theorem dist_div_div_le_of_le {E : Type u_6} [seminormed_comm_group E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} (h₁ : has_dist.dist a₁ b₁ ≤ r₁) (h₂ : has_dist.dist a₂ b₂ ≤ r₂) :
has_dist.dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂
source
theorem abs_dist_sub_le_dist_mul_mul {E : Type u_6} [seminormed_comm_group E] (a₁ a₂ b₁ b₂ : E) :
|has_dist.dist a₁ b₁ - has_dist.dist a₂ b₂| ≤ has_dist.dist (a₁ * a₂) (b₁ * b₂)
source
theorem abs_dist_sub_le_dist_add_add {E : Type u_6} [seminormed_add_comm_group E] (a₁ a₂ b₁ b₂ : E) :
|has_dist.dist a₁ b₁ - has_dist.dist a₂ b₂| ≤ has_dist.dist (a₁ + a₂) (b₁ + b₂)
source
theorem norm_multiset_sum_le {E : Type u_1} [seminormed_add_comm_group E] (m : multiset E) :
‖m.sum‖ ≤ (multiset.map (λ (x : E), ‖x‖) m).sum
source
theorem norm_multiset_prod_le {E : Type u_6} [seminormed_comm_group E] (m : multiset E) :
‖m.prod‖ ≤ (multiset.map (λ (x : E), ‖x‖) m).sum
source
theorem norm_sum_le {ι : Type u_4} {E : Type u_1} [seminormed_add_comm_group E] (s : finset ι) (f : ι → E) :
‖s.sum (λ (i : ι), f i)‖ ≤ s.sum (λ (i : ι), ‖f i‖)
source
theorem norm_prod_le {ι : Type u_4} {E : Type u_6} [seminormed_comm_group E] (s : finset ι) (f : ι → E) :
‖s.prod (λ (i : ι), f i)‖ ≤ s.sum (λ (i : ι), ‖f i‖)
source
theorem norm_prod_le_of_le {ι : Type u_4} {E : Type u_6} [seminormed_comm_group E] (s : finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ (b : ι), b ∈ s → ‖f b‖ ≤ n b) :
‖s.prod (λ (b : ι), f b)‖ ≤ s.sum (λ (b : ι), n b)
source
theorem norm_sum_le_of_le {ι : Type u_4} {E : Type u_6} [seminormed_add_comm_group E] (s : finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ (b : ι), b ∈ s → ‖f b‖ ≤ n b) :
‖s.sum (λ (b : ι), f b)‖ ≤ s.sum (λ (b : ι), n b)
source
theorem dist_sum_sum_le_of_le {ι : Type u_4} {E : Type u_6} [seminormed_add_comm_group E] (s : finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ (b : ι), b ∈ s → has_dist.dist (f b) (a b) ≤ d b) :
has_dist.dist (s.sum (λ (b : ι), f b)) (s.sum (λ (b : ι), a b)) ≤ s.sum (λ (b : ι), d b)
source
theorem dist_prod_prod_le_of_le {ι : Type u_4} {E : Type u_6} [seminormed_comm_group E] (s : finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ (b : ι), b ∈ s → has_dist.dist (f b) (a b) ≤ d b) :
has_dist.dist (s.prod (λ (b : ι), f b)) (s.prod (λ (b : ι), a b)) ≤ s.sum (λ (b : ι), d b)
source
theorem dist_sum_sum_le {ι : Type u_4} {E : Type u_6} [seminormed_add_comm_group E] (s : finset ι) (f a : ι → E) :
has_dist.dist (s.sum (λ (b : ι), f b)) (s.sum (λ (b : ι), a b)) ≤ s.sum (λ (b : ι), has_dist.dist (f b) (a b))
source
theorem dist_prod_prod_le {ι : Type u_4} {E : Type u_6} [seminormed_comm_group E] (s : finset ι) (f a : ι → E) :
has_dist.dist (s.prod (λ (b : ι), f b)) (s.prod (λ (b : ι), a b)) ≤ s.sum (λ (b : ι), has_dist.dist (f b) (a b))
source
theorem add_mem_ball_iff_norm {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} :
a + b ∈ metric.ball a r ↔ ‖b‖ < r
source
theorem mul_mem_ball_iff_norm {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} :
a * b ∈ metric.ball a r ↔ ‖b‖ < r
source
theorem mul_mem_closed_ball_iff_norm {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} :
a * b ∈ metric.closed_ball a r ↔ ‖b‖ ≤ r
source
theorem add_mem_closed_ball_iff_norm {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} :
a + b ∈ metric.closed_ball a r ↔ ‖b‖ ≤ r
source
@[simp]
theorem preimage_add_ball {E : Type u_6} [seminormed_add_comm_group E] (a b : E) (r : ℝ) :
has_add.add b ⁻¹' metric.ball a r = metric.ball (a - b) r
source
@[simp]
theorem preimage_mul_ball {E : Type u_6} [seminormed_comm_group E] (a b : E) (r : ℝ) :
has_mul.mul b ⁻¹' metric.ball a r = metric.ball (a / b) r
source
@[simp]
theorem preimage_add_closed_ball {E : Type u_6} [seminormed_add_comm_group E] (a b : E) (r : ℝ) :
has_add.add b ⁻¹' metric.closed_ball a r = metric.closed_ball (a - b) r
source
@[simp]
theorem preimage_mul_closed_ball {E : Type u_6} [seminormed_comm_group E] (a b : E) (r : ℝ) :
has_mul.mul b ⁻¹' metric.closed_ball a r = metric.closed_ball (a / b) r
source
@[simp]
theorem preimage_mul_sphere {E : Type u_6} [seminormed_comm_group E] (a b : E) (r : ℝ) :
has_mul.mul b ⁻¹' metric.sphere a r = metric.sphere (a / b) r
source
@[simp]
theorem preimage_add_sphere {E : Type u_6} [seminormed_add_comm_group E] (a b : E) (r : ℝ) :
has_add.add b ⁻¹' metric.sphere a r = metric.sphere (a - b) r
source
theorem norm_nsmul_le {E : Type u_6} [seminormed_add_comm_group E] (n : ℕ) (a : E) :
‖n • a‖ ≤ ↑n * ‖a‖
source
theorem norm_pow_le_mul_norm {E : Type u_6} [seminormed_comm_group E] (n : ℕ) (a : E) :
‖a ^ n‖ ≤ ↑n * ‖a‖
source
theorem nnnorm_pow_le_mul_norm {E : Type u_6} [seminormed_comm_group E] (n : ℕ) (a : E) :
‖a ^ n‖₊ ≤ ↑n * ‖a‖₊
source
theorem nnnorm_nsmul_le {E : Type u_6} [seminormed_add_comm_group E] (n : ℕ) (a : E) :
‖n • a‖₊ ≤ ↑n * ‖a‖₊
source
theorem pow_mem_closed_ball {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ metric.closed_ball b r) :
a ^ n ∈ metric.closed_ball (b ^ n) (n • r)
source
theorem nsmul_mem_closed_ball {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ metric.closed_ball b r) :
n • a ∈ metric.closed_ball (n • b) (n • r)
source
theorem pow_mem_ball {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ metric.ball b r) :
a ^ n ∈ metric.ball (b ^ n) (n • r)
source
theorem nsmul_mem_ball {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ metric.ball b r) :
n • a ∈ metric.ball (n • b) (n • r)
source
@[simp]
theorem add_mem_closed_ball_add_iff {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} {c : E} :
a + c ∈ metric.closed_ball (b + c) r ↔ a ∈ metric.closed_ball b r
source
@[simp]
theorem mul_mem_closed_ball_mul_iff {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} {c : E} :
a * c ∈ metric.closed_ball (b * c) r ↔ a ∈ metric.closed_ball b r
source
@[simp]
theorem add_mem_ball_add_iff {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} {c : E} :
a + c ∈ metric.ball (b + c) r ↔ a ∈ metric.ball b r
source
@[simp]
theorem mul_mem_ball_mul_iff {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} {c : E} :
a * c ∈ metric.ball (b * c) r ↔ a ∈ metric.ball b r
source
theorem vadd_closed_ball'' {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} :
a +ᵥ metric.closed_ball b r = metric.closed_ball (a +ᵥ b) r
source
theorem smul_closed_ball'' {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} :
a • metric.closed_ball b r = metric.closed_ball (a • b) r
source
theorem vadd_ball'' {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : ℝ} :
a +ᵥ metric.ball b r = metric.ball (a +ᵥ b) r
source
theorem smul_ball'' {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : ℝ} :
a • metric.ball b r = metric.ball (a • b) r
source
theorem controlled_sum_of_mem_closure {E : Type u_6} [seminormed_add_comm_group E] {a : E} {s : add_subgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :
∃ (v : ℕ → E), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), v i)) filter.at_top (nhds a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 - a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
source
theorem controlled_prod_of_mem_closure {E : Type u_6} [seminormed_comm_group E] {a : E} {s : subgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :
∃ (v : ℕ → E), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).prod (λ (i : ℕ), v i)) filter.at_top (nhds a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
source
theorem controlled_sum_of_mem_closure_range {E : Type u_6} {F : Type u_7} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {j : E →+ F} {b : F} (hb : b ∈ closure ↑(j.range)) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) :
∃ (a : ℕ → E), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), ⇑j (a i))) filter.at_top (nhds b) ∧ ‖⇑j (a 0) - b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖⇑j (a n)‖ < f n
source
theorem controlled_prod_of_mem_closure_range {E : Type u_6} {F : Type u_7} [seminormed_comm_group E] [seminormed_comm_group F] {j : E →* F} {b : F} (hb : b ∈ closure ↑(j.range)) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) :
∃ (a : ℕ → E), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).prod (λ (i : ℕ), ⇑j (a i))) filter.at_top (nhds b) ∧ ‖⇑j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖⇑j (a n)‖ < f n
source
theorem nndist_mul_mul_le {E : Type u_6} [seminormed_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_nndist.nndist (a₁ * a₂) (b₁ * b₂) ≤ has_nndist.nndist a₁ b₁ + has_nndist.nndist a₂ b₂
source
theorem nndist_add_add_le {E : Type u_6} [seminormed_add_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_nndist.nndist (a₁ + a₂) (b₁ + b₂) ≤ has_nndist.nndist a₁ b₁ + has_nndist.nndist a₂ b₂
source
theorem edist_add_add_le {E : Type u_6} [seminormed_add_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_edist.edist (a₁ + a₂) (b₁ + b₂) ≤ has_edist.edist a₁ b₁ + has_edist.edist a₂ b₂
source
theorem edist_mul_mul_le {E : Type u_6} [seminormed_comm_group E] (a₁ a₂ b₁ b₂ : E) :
has_edist.edist (a₁ * a₂) (b₁ * b₂) ≤ has_edist.edist a₁ b₁ + has_edist.edist a₂ b₂
source
theorem nnnorm_multiset_sum_le {E : Type u_6} [seminormed_add_comm_group E] (m : multiset E) :
‖m.sum‖₊ ≤ (multiset.map (λ (x : E), ‖x‖₊) m).sum
source
theorem nnnorm_multiset_prod_le {E : Type u_6} [seminormed_comm_group E] (m : multiset E) :
‖m.prod‖₊ ≤ (multiset.map (λ (x : E), ‖x‖₊) m).sum
source
theorem nnnorm_sum_le {ι : Type u_4} {E : Type u_6} [seminormed_add_comm_group E] (s : finset ι) (f : ι → E) :
‖s.sum (λ (a : ι), f a)‖₊ ≤ s.sum (λ (a : ι), ‖f a‖₊)
source
theorem nnnorm_prod_le {ι : Type u_4} {E : Type u_6} [seminormed_comm_group E] (s : finset ι) (f : ι → E) :
‖s.prod (λ (a : ι), f a)‖₊ ≤ s.sum (λ (a : ι), ‖f a‖₊)
source
theorem nnnorm_sum_le_of_le {ι : Type u_4} {E : Type u_6} [seminormed_add_comm_group E] (s : finset ι) {f : ι → E} {n : ι → nnreal} (h : ∀ (b : ι), b ∈ s → ‖f b‖₊ ≤ n b) :
‖s.sum (λ (b : ι), f b)‖₊ ≤ s.sum (λ (b : ι), n b)
source
theorem nnnorm_prod_le_of_le {ι : Type u_4} {E : Type u_6} [seminormed_comm_group E] (s : finset ι) {f : ι → E} {n : ι → nnreal} (h : ∀ (b : ι), b ∈ s → ‖f b‖₊ ≤ n b) :
‖s.prod (λ (b : ι), f b)‖₊ ≤ s.sum (λ (b : ι), n b)
source
@[protected, instance]
def real.has_norm  :
has_norm ℝ
Equations
source
@[simp]
theorem real.norm_eq_abs (r : ℝ) :
‖r‖ = |r|
source
@[protected, instance]
def real.normed_add_comm_group  :
normed_add_comm_group ℝ
Equations
source
theorem real.norm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
‖r‖ = r
source
theorem real.norm_of_nonpos {r : ℝ} (hr : r ≤ 0) :
‖r‖ = -r
source
theorem real.le_norm_self (r : ℝ) :
r ≤ ‖r‖
source
@[simp]
theorem real.norm_coe_nat (n : ℕ) :
‖↑n‖ = ↑n
source
@[simp]
theorem real.nnnorm_coe_nat (n : ℕ) :
‖↑n‖₊ = ↑n
source
@[simp]
theorem real.norm_two  :
‖2‖ = 2
source
@[simp]
theorem real.nnnorm_two  :
‖2‖₊ = 2
source
theorem real.nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
‖r‖₊ = ⟨r, hr⟩
source
@[simp]
theorem real.nnnorm_abs (r : ℝ) :
‖|r|‖₊ = ‖r‖₊
source
theorem real.ennnorm_eq_of_real {r : ℝ} (hr : 0 ≤ r) :
↑‖r‖₊ = ennreal.of_real r
source
theorem real.ennnorm_eq_of_real_abs (r : ℝ) :
↑‖r‖₊ = ennreal.of_real |r|
source
theorem real.to_nnreal_eq_nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
r.to_nnreal = ‖r‖₊
source
theorem real.of_real_le_ennnorm (r : ℝ) :
ennreal.of_real r ≤ ↑‖r‖₊
source
@[protected, instance]
def int.normed_add_comm_group  :
normed_add_comm_group ℤ
Equations
source
@[norm_cast]
theorem int.norm_cast_real (m : ℤ) :
‖↑m‖ = ‖m‖
source
theorem int.norm_eq_abs (n : ℤ) :
‖n‖ = |↑n|
source
@[simp]
theorem int.norm_coe_nat (n : ℕ) :
‖↑n‖ = ↑n
source
theorem nnreal.coe_nat_abs (n : ℤ) :
↑(n.nat_abs) = ‖n‖₊
source
theorem int.abs_le_floor_nnreal_iff (z : ℤ) (c : nnreal) :
|z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c
source
@[protected, instance]
def rat.normed_add_comm_group  :
normed_add_comm_group ℚ
Equations
source
@[simp, norm_cast]
theorem rat.norm_cast_real (r : ℚ) :
‖↑r‖ = ‖r‖
source
@[simp, norm_cast]
theorem int.norm_cast_rat (m : ℤ) :
‖↑m‖ = ‖m‖
source
theorem norm_zsmul_le {α : Type u_3} [seminormed_add_comm_group α] (n : ℤ) (a : α) :
‖n • a‖ ≤ ‖n‖ * ‖a‖
source
theorem norm_zpow_le_mul_norm {α : Type u_3} [seminormed_comm_group α] (n : ℤ) (a : α) :
‖a ^ n‖ ≤ ‖n‖ * ‖a‖
source
theorem nnnorm_zpow_le_mul_norm {α : Type u_3} [seminormed_comm_group α] (n : ℤ) (a : α) :
‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊
source
theorem nnnorm_zsmul_le {α : Type u_3} [seminormed_add_comm_group α] (n : ℤ) (a : α) :
‖n • a‖₊ ≤ ‖n‖₊ * ‖a‖₊
source
theorem lipschitz_with.inv {α : Type u_3} {E : Type u_6} [seminormed_comm_group E] [pseudo_emetric_space α] {K : nnreal} {f : α → E} (hf : lipschitz_with K f) :
lipschitz_with K (λ (x : α), (f x)⁻¹)
source
theorem lipschitz_with.neg {α : Type u_3} {E : Type u_6} [seminormed_add_comm_group E] [pseudo_emetric_space α] {K : nnreal} {f : α → E} (hf : lipschitz_with K f) :
lipschitz_with K (λ (x : α), -f x)
source
theorem lipschitz_with.mul' {α : Type u_3} {E : Type u_6} [seminormed_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x * g x)
source
theorem lipschitz_with.add {α : Type u_3} {E : Type u_6} [seminormed_add_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)
source
theorem lipschitz_with.div {α : Type u_3} {E : Type u_6} [seminormed_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x / g x)
source
theorem lipschitz_with.sub {α : Type u_3} {E : Type u_6} [seminormed_add_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)
source
theorem antilipschitz_with.mul_lipschitz_with {α : Type u_3} {E : Type u_6} [seminormed_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg g) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x * g x)
source
theorem antilipschitz_with.add_lipschitz_with {α : Type u_3} {E : Type u_6} [seminormed_add_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg g) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x + g x)
source
theorem antilipschitz_with.add_sub_lipschitz_with {α : Type u_3} {E : Type u_6} [seminormed_add_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg (g - f)) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ g
source
theorem antilipschitz_with.mul_div_lipschitz_with {α : Type u_3} {E : Type u_6} [seminormed_comm_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg (g / f)) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ g
source
theorem antilipschitz_with.le_mul_norm_sub {E : Type u_6} {F : Type u_7} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {K : nnreal} {f : E → F} (hf : antilipschitz_with K f) (x y : E) :
‖x - y‖ ≤ ↑K * ‖f x - f y‖
source
theorem antilipschitz_with.le_mul_norm_div {E : Type u_6} {F : Type u_7} [seminormed_comm_group E] [seminormed_comm_group F] {K : nnreal} {f : E → F} (hf : antilipschitz_with K f) (x y : E) :
‖x / y‖ ≤ ↑K * ‖f x / f y‖
source
@[protected, instance]
def seminormed_add_comm_group.to_has_lipschitz_add {E : Type u_6} [seminormed_add_comm_group E] :
has_lipschitz_add E
source
@[protected, instance]
def seminormed_comm_group.to_has_lipschitz_mul {E : Type u_6} [seminormed_comm_group E] :
has_lipschitz_mul E
source
@[protected, instance]
def seminormed_add_comm_group.to_uniform_add_group {E : Type u_6} [seminormed_add_comm_group E] :
uniform_add_group E

A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

source
@[protected, instance]
def seminormed_comm_group.to_uniform_group {E : Type u_6} [seminormed_comm_group E] :
uniform_group E

A seminormed group is a uniform group, i.e., multiplication and division are uniformly continuous.

source
@[protected, instance]
def seminormed_add_comm_group.to_topological_add_group {E : Type u_6} [seminormed_add_comm_group E] :
topological_add_group E
source
@[protected, instance]
def seminormed_comm_group.to_topological_group {E : Type u_6} [seminormed_comm_group E] :
topological_group E
source
theorem cauchy_seq_prod_of_eventually_eq {E : Type u_6} [seminormed_comm_group E] {u v : ℕ → E} {N : ℕ} (huv : ∀ (n : ℕ), n ≥ N → u n = v n) (hv : cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).prod (λ (k : ℕ), v k))) :
cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).prod (λ (k : ℕ), u k))
source
theorem cauchy_seq_sum_of_eventually_eq {E : Type u_6} [seminormed_add_comm_group E] {u v : ℕ → E} {N : ℕ} (huv : ∀ (n : ℕ), n ≥ N → u n = v n) (hv : cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), v k))) :
cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), u k))
source
@[simp]
theorem norm_eq_zero {E : Type u_6} [normed_add_group E] {a : E} :
‖a‖ = 0 ↔ a = 0
source
@[simp]
theorem norm_eq_zero'' {E : Type u_6} [normed_group E] {a : E} :
‖a‖ = 0 ↔ a = 1
source
theorem norm_ne_zero_iff' {E : Type u_6} [normed_group E] {a : E} :
‖a‖ ≠ 0 ↔ a ≠ 1
source
theorem norm_ne_zero_iff {E : Type u_6} [normed_add_group E] {a : E} :
‖a‖ ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem norm_pos_iff {E : Type u_6} [normed_add_group E] {a : E} :
0 < ‖a‖ ↔ a ≠ 0
source
@[simp]
theorem norm_pos_iff'' {E : Type u_6} [normed_group E] {a : E} :
0 < ‖a‖ ↔ a ≠ 1
source
@[simp]
theorem norm_le_zero_iff'' {E : Type u_6} [normed_group E] {a : E} :
‖a‖ ≤ 0 ↔ a = 1
source
@[simp]
theorem norm_le_zero_iff {E : Type u_6} [normed_add_group E] {a : E} :
‖a‖ ≤ 0 ↔ a = 0
source
theorem norm_div_eq_zero_iff {E : Type u_6} [normed_group E] {a b : E} :
‖a / b‖ = 0 ↔ a = b
source
theorem norm_sub_eq_zero_iff {E : Type u_6} [normed_add_group E] {a b : E} :
‖a - b‖ = 0 ↔ a = b
source
theorem norm_sub_pos_iff {E : Type u_6} [normed_add_group E] {a b : E} :
0 < ‖a - b‖ ↔ a ≠ b
source
theorem norm_div_pos_iff {E : Type u_6} [normed_group E] {a b : E} :
0 < ‖a / b‖ ↔ a ≠ b
source
theorem eq_of_norm_sub_le_zero {E : Type u_6} [normed_add_group E] {a b : E} (h : ‖a - b‖ ≤ 0) :
a = b
source
theorem eq_of_norm_div_le_zero {E : Type u_6} [normed_group E] {a b : E} (h : ‖a / b‖ ≤ 0) :
a = b
source
theorem eq_of_norm_div_eq_zero {E : Type u_6} [normed_group E] {a b : E} :
‖a / b‖ = 0 → a = b

Alias of the forward direction of norm_div_eq_zero_iff.

source
theorem eq_of_norm_sub_eq_zero {E : Type u_6} [normed_add_group E] {a b : E} :
‖a - b‖ = 0 → a = b

Alias of the forward direction of norm_div_eq_zero_iff.

source
@[simp]
theorem nnnorm_eq_zero' {E : Type u_6} [normed_group E] {a : E} :
‖a‖₊ = 0 ↔ a = 1
source
@[simp]
theorem nnnorm_eq_zero {E : Type u_6} [normed_add_group E] {a : E} :
‖a‖₊ = 0 ↔ a = 0
source
theorem nnnorm_ne_zero_iff' {E : Type u_6} [normed_group E] {a : E} :
‖a‖₊ ≠ 0 ↔ a ≠ 1
source
theorem nnnorm_ne_zero_iff {E : Type u_6} [normed_add_group E] {a : E} :
‖a‖₊ ≠ 0 ↔ a ≠ 0
source
theorem tendsto_norm_sub_self_punctured_nhds {E : Type u_6} [normed_add_group E] (a : E) :
filter.tendsto (λ (x : E), ‖x - a‖) (nhds_within a {a}ᶜ) (nhds_within 0 (set.Ioi 0))
source
theorem tendsto_norm_div_self_punctured_nhds {E : Type u_6} [normed_group E] (a : E) :
filter.tendsto (λ (x : E), ‖x / a‖) (nhds_within a {a}ᶜ) (nhds_within 0 (set.Ioi 0))
source
theorem tendsto_norm_nhds_within_zero {E : Type u_6} [normed_add_group E] :
filter.tendsto has_norm.norm (nhds_within 0 {0}ᶜ) (nhds_within 0 (set.Ioi 0))
source
theorem tendsto_norm_nhds_within_one {E : Type u_6} [normed_group E] :
filter.tendsto has_norm.norm (nhds_within 1 {1}ᶜ) (nhds_within 0 (set.Ioi 0))
source
def norm_group_norm (E : Type u_6) [normed_group E] :
group_norm E

The norm of a normed group as a group norm.

Equations
source
def norm_add_group_norm (E : Type u_6) [normed_add_group E] :
add_group_norm E

The norm of a normed group as an additive group norm.

Equations
source
@[simp]
theorem coe_norm_group_norm (E : Type u_6) [normed_group E] :
⇑(norm_group_norm E) = has_norm.norm

Some relations with has_compact_support

source
theorem has_compact_support_norm_iff {α : Type u_3} {E : Type u_6} [normed_add_group E] [topological_space α] {f : α → E} :
has_compact_support (λ (x : α), ‖f x‖) ↔ has_compact_support f
source
theorem has_compact_support.norm {α : Type u_3} {E : Type u_6} [normed_add_group E] [topological_space α] {f : α → E} :
has_compact_support f → has_compact_support (λ (x : α), ‖f x‖)

Alias of the reverse direction of has_compact_support_norm_iff.

source
theorem continuous.bounded_above_of_compact_support {α : Type u_3} {E : Type u_6} [normed_add_group E] [topological_space α] {f : α → E} (hf : continuous f) (h : has_compact_support f) :
∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C
source
theorem has_compact_mul_support.exists_pos_le_norm {α : Type u_3} {E : Type u_6} [normed_add_group α] {f : α → E} [has_one E] (hf : has_compact_mul_support f) :
∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
source
theorem has_compact_support.exists_pos_le_norm {α : Type u_3} {E : Type u_6} [normed_add_group α] {f : α → E} [has_zero E] (hf : has_compact_support f) :
∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 0

ulift #

source
@[protected, instance]
def ulift.has_norm {E : Type u_6} [has_norm E] :
has_norm (ulift E)
Equations
source
theorem ulift.norm_def {E : Type u_6} [has_norm E] (x : ulift E) :
‖x‖ = ‖x.down‖
source
@[simp]
theorem ulift.norm_up {E : Type u_6} [has_norm E] (x : E) :
‖{down := x}‖ = ‖x‖
source
@[simp]
theorem ulift.norm_down {E : Type u_6} [has_norm E] (x : ulift E) :
‖x.down‖ = ‖x‖
source
@[protected, instance]
def ulift.has_nnnorm {E : Type u_6} [has_nnnorm E] :
has_nnnorm (ulift E)
Equations
source
theorem ulift.nnnorm_def {E : Type u_6} [has_nnnorm E] (x : ulift E) :
‖x‖₊ = ‖x.down‖₊
source
@[simp]
theorem ulift.nnnorm_up {E : Type u_6} [has_nnnorm E] (x : E) :
‖{down := x}‖₊ = ‖x‖₊
source
@[simp]
theorem ulift.nnnorm_down {E : Type u_6} [has_nnnorm E] (x : ulift E) :
‖x.down‖₊ = ‖x‖₊
source
@[protected, instance]
def ulift.seminormed_add_group {E : Type u_6} [seminormed_add_group E] :
seminormed_add_group (ulift E)
Equations
source
@[protected, instance]
def ulift.seminormed_group {E : Type u_6} [seminormed_group E] :
seminormed_group (ulift E)
Equations
source
@[protected, instance]
def ulift.seminormed_comm_group {E : Type u_6} [seminormed_comm_group E] :
seminormed_comm_group (ulift E)
Equations
source
@[protected, instance]
def ulift.seminormed_add_comm_group {E : Type u_6} [seminormed_add_comm_group E] :
seminormed_add_comm_group (ulift E)
Equations
source
@[protected, instance]
def ulift.normed_group {E : Type u_6} [normed_group E] :
normed_group (ulift E)
Equations
source
@[protected, instance]
def ulift.normed_add_group {E : Type u_6} [normed_add_group E] :
normed_add_group (ulift E)
Equations
source
@[protected, instance]
def ulift.normed_add_comm_group {E : Type u_6} [normed_add_comm_group E] :
normed_add_comm_group (ulift E)
Equations
source
@[protected, instance]
def ulift.normed_comm_group {E : Type u_6} [normed_comm_group E] :
normed_comm_group (ulift E)
Equations

additive, multiplicative #

source
@[protected, instance]
def additive.has_norm {E : Type u_6} [has_norm E] :
has_norm (additive E)
Equations
source
@[protected, instance]
def multiplicative.has_norm {E : Type u_6} [has_norm E] :
has_norm (multiplicative E)
Equations
source
@[simp]
theorem norm_to_mul {E : Type u_6} [has_norm E] (x : additive E) :
‖⇑additive.to_mul x‖ = ‖x‖
source
@[simp]
theorem norm_of_mul {E : Type u_6} [has_norm E] (x : E) :
‖⇑additive.of_mul x‖ = ‖x‖
source
@[simp]
theorem norm_to_add {E : Type u_6} [has_norm E] (x : multiplicative E) :
‖⇑multiplicative.to_add x‖ = ‖x‖
source
@[simp]
theorem norm_of_add {E : Type u_6} [has_norm E] (x : E) :
‖⇑multiplicative.of_add x‖ = ‖x‖
source
@[protected, instance]
def additive.has_nnnorm {E : Type u_6} [has_nnnorm E] :
has_nnnorm (additive E)
Equations
source
@[protected, instance]
def multiplicative.has_nnnorm {E : Type u_6} [has_nnnorm E] :
has_nnnorm (multiplicative E)
Equations
source
@[simp]
theorem nnnorm_to_mul {E : Type u_6} [has_nnnorm E] (x : additive E) :
‖⇑additive.to_mul x‖₊ = ‖x‖₊
source
@[simp]
theorem nnnorm_of_mul {E : Type u_6} [has_nnnorm E] (x : E) :
‖⇑additive.of_mul x‖₊ = ‖x‖₊
source
@[simp]
theorem nnnorm_to_add {E : Type u_6} [has_nnnorm E] (x : multiplicative E) :
‖⇑multiplicative.to_add x‖₊ = ‖x‖₊
source
@[simp]
theorem nnnorm_of_add {E : Type u_6} [has_nnnorm E] (x : E) :
‖⇑multiplicative.of_add x‖₊ = ‖x‖₊
source
@[protected, instance]
def additive.seminormed_add_group {E : Type u_6} [seminormed_group E] :
seminormed_add_group (additive E)
Equations
source
@[protected, instance]
def multiplicative.seminormed_group {E : Type u_6} [seminormed_add_group E] :
seminormed_group (multiplicative E)
Equations
source
@[protected, instance]
def additive.seminormed_add_comm_group {E : Type u_6} [seminormed_comm_group E] :
seminormed_add_comm_group (additive E)
Equations
source
@[protected, instance]
def multiplicative.seminormed_comm_group {E : Type u_6} [seminormed_add_comm_group E] :
seminormed_comm_group (multiplicative E)
Equations
source
@[protected, instance]
def additive.normed_add_group {E : Type u_6} [normed_group E] :
normed_add_group (additive E)
Equations
source
@[protected, instance]
def multiplicative.normed_group {E : Type u_6} [normed_add_group E] :
normed_group (multiplicative E)
Equations
source
@[protected, instance]
def additive.normed_add_comm_group {E : Type u_6} [normed_comm_group E] :
normed_add_comm_group (additive E)
Equations
source
@[protected, instance]
def multiplicative.normed_comm_group {E : Type u_6} [normed_add_comm_group E] :
normed_comm_group (multiplicative E)
Equations

Order dual #

source
@[protected, instance]
def order_dual.has_norm {E : Type u_6} [has_norm E] :
has_norm Eᵒᵈ
Equations
source
@[simp]
theorem norm_to_dual {E : Type u_6} [has_norm E] (x : E) :
‖⇑order_dual.to_dual x‖ = ‖x‖
source
@[simp]
theorem norm_of_dual {E : Type u_6} [has_norm E] (x : Eᵒᵈ) :
‖⇑order_dual.of_dual x‖ = ‖x‖
source
@[protected, instance]
def order_dual.has_nnnorm {E : Type u_6} [has_nnnorm E] :
has_nnnorm Eᵒᵈ
Equations
source
@[simp]
theorem nnnorm_to_dual {E : Type u_6} [has_nnnorm E] (x : E) :
‖⇑order_dual.to_dual x‖₊ = ‖x‖₊
source
@[simp]
theorem nnnorm_of_dual {E : Type u_6} [has_nnnorm E] (x : Eᵒᵈ) :
‖⇑order_dual.of_dual x‖₊ = ‖x‖₊
source
@[protected, instance]
def order_dual.seminormed_group {E : Type u_6} [seminormed_group E] :
seminormed_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.seminormed_add_group {E : Type u_6} [seminormed_add_group E] :
seminormed_add_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.seminormed_comm_group {E : Type u_6} [seminormed_comm_group E] :
seminormed_comm_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.seminormed_add_comm_group {E : Type u_6} [seminormed_add_comm_group E] :
seminormed_add_comm_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.normed_add_group {E : Type u_6} [normed_add_group E] :
normed_add_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.normed_group {E : Type u_6} [normed_group E] :
normed_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.normed_add_comm_group {E : Type u_6} [normed_add_comm_group E] :
normed_add_comm_group Eᵒᵈ
Equations
source
@[protected, instance]
def order_dual.normed_comm_group {E : Type u_6} [normed_comm_group E] :
normed_comm_group Eᵒᵈ
Equations

Binary product of normed groups #

source
@[protected, instance]
def prod.has_norm {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] :
has_norm (E × F)
Equations
source
theorem prod.norm_def {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] (x : E × F) :
‖x‖ = linear_order.max ‖x.fst‖ ‖x.snd‖
source
theorem norm_fst_le {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] (x : E × F) :
‖x.fst‖ ≤ ‖x‖
source
theorem norm_snd_le {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] (x : E × F) :
‖x.snd‖ ≤ ‖x‖
source
theorem norm_prod_le_iff {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] {x : E × F} {r : ℝ} :
‖x‖ ≤ r ↔ ‖x.fst‖ ≤ r ∧ ‖x.snd‖ ≤ r
source
@[protected, instance]
def prod.seminormed_add_group {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] :
seminormed_add_group (E × F)

Product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def prod.seminormed_group {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] :
seminormed_group (E × F)

Product of seminormed groups, using the sup norm.

Equations
source
theorem prod.nnorm_def {E : Type u_6} {F : Type u_7} [seminormed_group E] [seminormed_group F] (x : E × F) :
‖x‖₊ = linear_order.max ‖x.fst‖₊ ‖x.snd‖₊
source
theorem prod.nnnorm_def' {E : Type u_6} {F : Type u_7} [seminormed_add_group E] [seminormed_add_group F] (x : E × F) :
‖x‖₊ = linear_order.max ‖x.fst‖₊ ‖x.snd‖₊
source
@[protected, instance]
def prod.seminormed_add_comm_group {E : Type u_6} {F : Type u_7} [seminormed_add_comm_group E] [seminormed_add_comm_group F] :
seminormed_add_comm_group (E × F)

Product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def prod.seminormed_comm_group {E : Type u_6} {F : Type u_7} [seminormed_comm_group E] [seminormed_comm_group F] :
seminormed_comm_group (E × F)

Product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def prod.normed_group {E : Type u_6} {F : Type u_7} [normed_group E] [normed_group F] :
normed_group (E × F)

Product of normed groups, using the sup norm.

Equations
source
@[protected, instance]
def prod.normed_add_group {E : Type u_6} {F : Type u_7} [normed_add_group E] [normed_add_group F] :
normed_add_group (E × F)

Product of normed groups, using the sup norm.

Equations
source
@[protected, instance]
def prod.normed_comm_group {E : Type u_6} {F : Type u_7} [normed_comm_group E] [normed_comm_group F] :
normed_comm_group (E × F)

Product of normed groups, using the sup norm.

Equations
source
@[protected, instance]
def prod.normed_add_comm_group {E : Type u_6} {F : Type u_7} [normed_add_comm_group E] [normed_add_comm_group F] :
normed_add_comm_group (E × F)

Product of normed groups, using the sup norm.

Equations

Finite product of normed groups #

source
@[protected, instance]
def pi.seminormed_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] :
seminormed_group (Π (i : ι), π i)

Finite product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def pi.seminormed_add_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] :
seminormed_add_group (Π (i : ι), π i)

Finite product of seminormed groups, using the sup norm.

Equations
source
theorem pi.norm_def' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) :
‖f‖ = ↑(finset.univ.sup (λ (b : ι), ‖f b‖₊))
source
theorem pi.norm_def {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) :
‖f‖ = ↑(finset.univ.sup (λ (b : ι), ‖f b‖₊))
source
theorem pi.nnnorm_def {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) :
‖f‖₊ = finset.univ.sup (λ (b : ι), ‖f b‖₊)
source
theorem pi.nnnorm_def' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) :
‖f‖₊ = finset.univ.sup (λ (b : ι), ‖f b‖₊)
source
theorem pi_norm_le_iff_of_nonneg {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] {x : Π (i : ι), π i} {r : ℝ} (hr : 0 ≤ r) :
‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

source
theorem pi_norm_le_iff_of_nonneg' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] {x : Π (i : ι), π i} {r : ℝ} (hr : 0 ≤ r) :
‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

source
theorem pi_nnnorm_le_iff {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] {x : Π (i : ι), π i} {r : nnreal} :
‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r
source
theorem pi_nnnorm_le_iff' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] {x : Π (i : ι), π i} {r : nnreal} :
‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r
source
theorem pi_norm_le_iff_of_nonempty {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) {r : ℝ} [nonempty ι] :
‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
source
theorem pi_norm_le_iff_of_nonempty' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) {r : ℝ} [nonempty ι] :
‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
source
theorem pi_norm_lt_iff' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] {x : Π (i : ι), π i} {r : ℝ} (hr : 0 < r) :
‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

source
theorem pi_norm_lt_iff {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] {x : Π (i : ι), π i} {r : ℝ} (hr : 0 < r) :
‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

source
theorem pi_nnnorm_lt_iff {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] {x : Π (i : ι), π i} {r : nnreal} (hr : 0 < r) :
‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r
source
theorem pi_nnnorm_lt_iff' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] {x : Π (i : ι), π i} {r : nnreal} (hr : 0 < r) :
‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r
source
theorem norm_le_pi_norm {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) (i : ι) :
‖f i‖ ≤ ‖f‖
source
theorem norm_le_pi_norm' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) (i : ι) :
‖f i‖ ≤ ‖f‖
source
theorem nnnorm_le_pi_nnnorm {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) (i : ι) :
‖f i‖₊ ≤ ‖f‖₊
source
theorem nnnorm_le_pi_nnnorm' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) (i : ι) :
‖f i‖₊ ≤ ‖f‖₊
source
theorem pi_norm_const_le {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] (a : E) :
‖(λ (_x : ι), a)‖ ≤ ‖a‖
source
theorem pi_norm_const_le' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] (a : E) :
‖(λ (_x : ι), a)‖ ≤ ‖a‖
source
theorem pi_nnnorm_const_le' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] (a : E) :
‖(λ (_x : ι), a)‖₊ ≤ ‖a‖₊
source
theorem pi_nnnorm_const_le {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] (a : E) :
‖(λ (_x : ι), a)‖₊ ≤ ‖a‖₊
source
@[simp]
theorem pi_norm_const {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] [nonempty ι] (a : E) :
‖(λ (i : ι), a)‖ = ‖a‖
source
@[simp]
theorem pi_norm_const' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] [nonempty ι] (a : E) :
‖(λ (i : ι), a)‖ = ‖a‖
source
@[simp]
theorem pi_nnnorm_const' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] [nonempty ι] (a : E) :
‖(λ (i : ι), a)‖₊ = ‖a‖₊
source
@[simp]
theorem pi_nnnorm_const {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] [nonempty ι] (a : E) :
‖(λ (i : ι), a)‖₊ = ‖a‖₊
source
theorem pi.sum_norm_apply_le_norm' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), ‖f i‖) ≤ fintype.card ι • ‖f‖

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

source
theorem pi.sum_norm_apply_le_norm {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), ‖f i‖) ≤ fintype.card ι • ‖f‖

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

source
theorem pi.sum_nnnorm_apply_le_nnnorm' {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), ‖f i‖₊) ≤ fintype.card ι • ‖f‖₊

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

source
theorem pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), ‖f i‖₊) ≤ fintype.card ι • ‖f‖₊

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

source
@[protected, instance]
def pi.seminormed_comm_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_comm_group (π i)] :
seminormed_comm_group (Π (i : ι), π i)

Finite product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def pi.seminormed_add_comm_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] :
seminormed_add_comm_group (Π (i : ι), π i)

Finite product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def pi.normed_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), normed_group (π i)] :
normed_group (Π (i : ι), π i)

Finite product of normed groups, using the sup norm.

Equations
source
@[protected, instance]
def pi.normed_add_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), normed_add_group (π i)] :
normed_add_group (Π (i : ι), π i)

Finite product of seminormed groups, using the sup norm.

Equations
source
@[protected, instance]
def pi.normed_comm_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), normed_comm_group (π i)] :
normed_comm_group (Π (i : ι), π i)

Finite product of normed groups, using the sup norm.

Equations
source
@[protected, instance]
def pi.normed_add_comm_group {ι : Type u_4} {π : ι → Type u_9} [fintype ι] [Π (i : ι), normed_add_comm_group (π i)] :
normed_add_comm_group (Π (i : ι), π i)

Finite product of seminormed groups, using the sup norm.

Equations

Multiplicative opposite #

source
@[protected, instance]
def mul_opposite.seminormed_add_group {E : Type u_6} [seminormed_add_group E] :
seminormed_add_group Eᵐᵒᵖ

The (additive) norm on the multiplicative opposite is the same as the norm on the original type.

Note that we do not provide this more generally as has_norm Eᵐᵒᵖ, as this is not always a good choice of norm in the multiplicative seminormed_group E case.

We could repeat this instance to provide a [seminormed_group E] : seminormed_group Eᵃᵒᵖ instance, but that case would likely never be used.

Equations
source
theorem mul_opposite.norm_op {E : Type u_6} [seminormed_add_group E] (a : E) :
‖mul_opposite.op a‖ = ‖a‖
source
theorem mul_opposite.norm_unop {E : Type u_6} [seminormed_add_group E] (a : Eᵐᵒᵖ) :
‖mul_opposite.unop a‖ = ‖a‖
source
theorem mul_opposite.nnnorm_op {E : Type u_6} [seminormed_add_group E] (a : E) :
‖mul_opposite.op a‖₊ = ‖a‖₊
source
theorem mul_opposite.nnnorm_unop {E : Type u_6} [seminormed_add_group E] (a : Eᵐᵒᵖ) :
‖mul_opposite.unop a‖₊ = ‖a‖₊
source
@[protected, instance]
def mul_opposite.normed_add_group {E : Type u_6} [normed_add_group E] :
normed_add_group Eᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.seminormed_add_comm_group {E : Type u_6} [seminormed_add_comm_group E] :
seminormed_add_comm_group Eᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.normed_add_comm_group {E : Type u_6} [normed_add_comm_group E] :
normed_add_comm_group Eᵐᵒᵖ
Equations

Subgroups of normed groups #

source
@[protected, instance]
def subgroup.seminormed_group {E : Type u_6} [seminormed_group E] {s : subgroup E} :
seminormed_group ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations
source
@[protected, instance]
def add_subgroup.seminormed_add_group {E : Type u_6} [seminormed_add_group E] {s : add_subgroup E} :
seminormed_add_group ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations
source
@[simp]
theorem subgroup.coe_norm {E : Type u_6} [seminormed_group E] {s : subgroup E} (x : ↥s) :
‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

source
@[simp]
theorem add_subgroup.coe_norm {E : Type u_6} [seminormed_add_group E] {s : add_subgroup E} (x : ↥s) :
‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

source
@[norm_cast]
theorem add_subgroup.norm_coe {E : Type u_6} [seminormed_add_group E] {s : add_subgroup E} (x : ↥s) :
‖↑x‖ = ‖x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

This is a reversed version of the simp lemma add_subgroup.coe_norm for use by norm_cast.

source
@[norm_cast]
theorem subgroup.norm_coe {E : Type u_6} [seminormed_group E] {s : subgroup E} (x : ↥s) :
‖↑x‖ = ‖x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

This is a reversed version of the simp lemma subgroup.coe_norm for use by norm_cast.

source
@[protected, instance]
def add_subgroup.seminormed_add_comm_group {E : Type u_6} [seminormed_add_comm_group E] {s : add_subgroup E} :
seminormed_add_comm_group ↥s
Equations
source
@[protected, instance]
def subgroup.seminormed_comm_group {E : Type u_6} [seminormed_comm_group E] {s : subgroup E} :
seminormed_comm_group ↥s
Equations
source
@[protected, instance]
def subgroup.normed_group {E : Type u_6} [normed_group E] {s : subgroup E} :
normed_group ↥s
Equations
source
@[protected, instance]
def add_subgroup.normed_add_group {E : Type u_6} [normed_add_group E] {s : add_subgroup E} :
normed_add_group ↥s
Equations
source
@[protected, instance]
def subgroup.normed_comm_group {E : Type u_6} [normed_comm_group E] {s : subgroup E} :
normed_comm_group ↥s
Equations
source
@[protected, instance]
def add_subgroup.normed_add_comm_group {E : Type u_6} [normed_add_comm_group E] {s : add_subgroup E} :
normed_add_comm_group ↥s
Equations

Submodules of normed groups #

source
@[protected, instance]
def submodule.seminormed_add_comm_group {𝕜 : Type u_2} {E : Type u_6} {_x : ring 𝕜} [seminormed_add_comm_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :
seminormed_add_comm_group ↥s

A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations
source
@[simp]
theorem submodule.coe_norm {𝕜 : Type u_2} {E : Type u_6} {_x : ring 𝕜} [seminormed_add_comm_group E] {_x_1 : module 𝕜 E} {s : submodule 𝕜 E} (x : ↥s) :
‖x‖ = ‖↑x‖

If x is an element of a submodule s of a normed group E, its norm in s is equal to its norm in E.

source
@[norm_cast]
theorem submodule.norm_coe {𝕜 : Type u_2} {E : Type u_6} {_x : ring 𝕜} [seminormed_add_comm_group E] {_x_1 : module 𝕜 E} {s : submodule 𝕜 E} (x : ↥s) :
‖↑x‖ = ‖x‖

If x is an element of a submodule s of a normed group E, its norm in E is equal to its norm in s.

This is a reversed version of the simp lemma submodule.coe_norm for use by norm_cast.

source
@[protected, instance]
def submodule.normed_add_comm_group {𝕜 : Type u_2} {E : Type u_6} {_x : ring 𝕜} [normed_add_comm_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :
normed_add_comm_group ↥s

A submodule of a normed group is also a normed group, with the restriction of the norm.

Equations