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