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

@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[reducible]
def normed_group.of_separation {E : Type u_6} [seminormed_group E] (h : (x : E), x = 0 x = 1) :

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

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

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

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
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)) :

Construct a seminormed group from a translation-invariant distance.

Equations
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)) :

Construct a seminormed group from a multiplication-invariant distance.

Equations
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) :

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
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) :

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
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)) :

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
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) :

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
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)) :

Construct a normed group from a multiplication-invariant distance.

Equations
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)) :

Construct a normed group from a translation-invariant distance.

Equations
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) :

Construct a normed group from a translation-invariant pseudodistance.

Equations
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) :

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
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)) :

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
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)) :

Construct a normed group from a translation-invariant pseudodistance.

Equations
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) :

Construct a normed group from a translation-invariant pseudodistance.

Equations
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) :

Construct a normed group from a multiplication-invariant pseudodistance.

Equations

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

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

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

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

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

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

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

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
@[simp]
theorem punit.norm_eq_zero (r : punit) :
theorem dist_eq_norm_sub {E : Type u_6} [seminormed_add_group E] (a b : E) :
theorem dist_eq_norm_div {E : Type u_6} [seminormed_group E] (a b : E) :
theorem dist_eq_norm_sub' {E : Type u_6} [seminormed_add_group E] (a b : E) :
theorem dist_eq_norm_div' {E : Type u_6} [seminormed_group E] (a b : E) :
theorem dist_eq_norm {E : Type u_6} [seminormed_add_group E] (a b : E) :

Alias of dist_eq_norm_sub.

theorem dist_eq_norm' {E : Type u_6} [seminormed_add_group E] (a b : E) :

Alias of dist_eq_norm_sub'.

@[simp]
theorem dist_one_right {E : Type u_6} [seminormed_group E] (a : E) :
@[simp]
theorem dist_zero_right {E : Type u_6} [seminormed_add_group E] (a : E) :
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) :
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) :
theorem norm_sub_rev {E : Type u_6} [seminormed_add_group E] (a b : E) :
a - b = b - a
theorem norm_div_rev {E : Type u_6} [seminormed_group E] (a b : E) :
a / b = b / a
@[simp]
theorem norm_inv' {E : Type u_6} [seminormed_group E] (a : E) :
@[simp]
theorem norm_neg {E : Type u_6} [seminormed_add_group E] (a : E) :
@[simp]
theorem dist_mul_self_right {E : Type u_6} [seminormed_group E] (a b : E) :
@[simp]
theorem dist_add_self_right {E : Type u_6} [seminormed_add_group E] (a b : E) :
@[simp]
theorem dist_add_self_left {E : Type u_6} [seminormed_add_group E] (a b : E) :
@[simp]
theorem dist_mul_self_left {E : Type u_6} [seminormed_group E] (a b : E) :
@[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)
@[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)
@[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
@[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

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.

theorem norm_add_le {E : Type u_6} [seminormed_add_group E] (a b : E) :

Triangle inequality for the norm.

theorem norm_mul_le' {E : Type u_6} [seminormed_group E] (a b : E) :

Triangle inequality for the norm.

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₂
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₂
theorem norm_add₃_le {E : Type u_6} [seminormed_add_group E] (a b c : E) :
theorem norm_mul₃_le {E : Type u_6} [seminormed_group E] (a b c : E) :
@[simp]
theorem norm_nonneg {E : Type u_6} [seminormed_add_group E] (a : E) :
@[simp]
theorem norm_nonneg' {E : Type u_6} [seminormed_group E] (a : E) :

Extension for the positivity tactic: norms are nonnegative.

@[simp]
theorem norm_zero {E : Type u_6} [seminormed_add_group E] :
@[simp]
theorem norm_one' {E : Type u_6} [seminormed_group E] :
theorem ne_zero_of_norm_ne_zero {E : Type u_6} [seminormed_add_group E] {a : E} :
a 0 a 0
theorem ne_one_of_norm_ne_zero {E : Type u_6} [seminormed_group E] {a : E} :
a 0 a 1
theorem norm_of_subsingleton {E : Type u_6} [seminormed_add_group E] [subsingleton E] (a : E) :
theorem norm_of_subsingleton' {E : Type u_6} [seminormed_group E] [subsingleton E] (a : E) :
theorem zero_lt_one_add_norm_sq {E : Type u_6} [seminormed_add_group E] (x : E) :
0 < 1 + x ^ 2
theorem zero_lt_one_add_norm_sq' {E : Type u_6} [seminormed_group E] (x : E) :
0 < 1 + x ^ 2
theorem norm_sub_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
theorem norm_div_le {E : Type u_6} [seminormed_group E] (a b : E) :
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₂
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₂
theorem abs_norm_sub_norm_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
theorem abs_norm_sub_norm_le' {E : Type u_6} [seminormed_group E] (a b : E) :
theorem norm_sub_norm_le' {E : Type u_6} [seminormed_group E] (a b : E) :
theorem norm_sub_norm_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
theorem norm_le_norm_add_norm_div' {E : Type u_6} [seminormed_group E] (u v : E) :
theorem norm_le_norm_add_norm_div {E : Type u_6} [seminormed_group E] (u v : E) :
theorem norm_le_insert' {E : Type u_6} [seminormed_add_group E] (u v : E) :

Alias of norm_le_norm_add_norm_sub'.

theorem norm_le_insert {E : Type u_6} [seminormed_add_group E] (u v : E) :

Alias of norm_le_norm_add_norm_sub.

theorem norm_le_add_norm_add {E : Type u_6} [seminormed_add_group E] (u v : E) :
theorem norm_le_mul_norm_add {E : Type u_6} [seminormed_group E] (u v : E) :
theorem ball_eq {E : Type u_6} [seminormed_add_group E] (y : E) (ε : ) :
metric.ball y ε = {x : E | x - y < ε}
theorem ball_eq' {E : Type u_6} [seminormed_group E] (y : E) (ε : ) :
metric.ball y ε = {x : E | x / y < ε}
theorem ball_zero_eq {E : Type u_6} [seminormed_add_group E] (r : ) :
metric.ball 0 r = {x : E | x < r}
theorem ball_one_eq {E : Type u_6} [seminormed_group E] (r : ) :
metric.ball 1 r = {x : E | x < r}
theorem mem_ball_iff_norm'' {E : Type u_6} [seminormed_group E] {a b : E} {r : } :
theorem mem_ball_iff_norm {E : Type u_6} [seminormed_add_group E] {a b : E} {r : } :
theorem mem_ball_iff_norm' {E : Type u_6} [seminormed_add_group E] {a b : E} {r : } :
theorem mem_ball_iff_norm''' {E : Type u_6} [seminormed_group E] {a b : E} {r : } :
@[simp]
theorem mem_ball_zero_iff {E : Type u_6} [seminormed_add_group E] {a : E} {r : } :
@[simp]
theorem mem_ball_one_iff {E : Type u_6} [seminormed_group E] {a : E} {r : } :
theorem mem_closed_ball_iff_norm'' {E : Type u_6} [seminormed_group E] {a b : E} {r : } :
theorem mem_closed_ball_iff_norm {E : Type u_6} [seminormed_add_group E] {a b : E} {r : } :
@[simp]
theorem mem_closed_ball_one_iff {E : Type u_6} [seminormed_group E] {a : E} {r : } :
@[simp]
theorem mem_closed_ball_zero_iff {E : Type u_6} [seminormed_add_group E] {a : E} {r : } :
theorem mem_closed_ball_iff_norm''' {E : Type u_6} [seminormed_group E] {a b : E} {r : } :
theorem mem_closed_ball_iff_norm' {E : Type u_6} [seminormed_add_group E] {a b : E} {r : } :
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) :
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) :
theorem norm_lt_of_mem_ball {E : Type u_6} [seminormed_add_group E] {a b : E} {r : } (h : b metric.ball a r) :
theorem norm_lt_of_mem_ball' {E : Type u_6} [seminormed_group E] {a b : E} {r : } (h : b metric.ball a r) :
theorem norm_div_sub_norm_div_le_norm_div {E : Type u_6} [seminormed_group E] (u v w : E) :
theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_6} [seminormed_add_group E] (u v w : E) :
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
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
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'.

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.

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
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
@[simp]
theorem mem_sphere_iff_norm {E : Type u_6} [seminormed_add_group E] {a b : E} {r : } :
@[simp]
theorem mem_sphere_iff_norm' {E : Type u_6} [seminormed_group E] {a b : E} {r : } :
@[simp]
theorem mem_sphere_one_iff_norm {E : Type u_6} [seminormed_group E] {a : E} {r : } :
@[simp]
theorem mem_sphere_zero_iff_norm {E : Type u_6} [seminormed_add_group E] {a : E} {r : } :
@[simp]
theorem norm_eq_of_mem_sphere' {E : Type u_6} [seminormed_group E] {r : } (x : (metric.sphere 1 r)) :
@[simp]
theorem norm_eq_of_mem_sphere {E : Type u_6} [seminormed_add_group E] {r : } (x : (metric.sphere 0 r)) :
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
theorem ne_one_of_mem_sphere {E : Type u_6} [seminormed_group E] {r : } (hr : r 0) (x : (metric.sphere 1 r)) :
x 1

The norm of a seminormed group as a group seminorm.

Equations

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

Equations
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 < ε)
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 < ε)
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 < ε)
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 < ε)
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 < ε)
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 < ε)
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 < ε})
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 < ε})
theorem normed_comm_group.nhds_one_basis_norm_lt {E : Type u_6} [seminormed_group E] :
(nhds 1).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {y : E | y < ε})
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 < ε})
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 < ε})
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 < ε})
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) :

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.

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) :

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.

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
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
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.

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.

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
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
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
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
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.

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.

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
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
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) :

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‖.

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) :

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‖

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) :
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) :
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
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
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 : 𝓕) :
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 : 𝓕) :
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.

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.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_nnnorm' {E : Type u_6} [seminormed_group E] (a : E) :
@[simp, norm_cast]
theorem coe_nnnorm {E : Type u_6} [seminormed_add_group E] (a : E) :
theorem norm_to_nnreal' {E : Type u_6} [seminormed_group E] {a : E} :
theorem nndist_eq_nnnorm_div {E : Type u_6} [seminormed_group E] (a b : E) :
@[simp]
theorem nnnorm_zero {E : Type u_6} [seminormed_add_group E] :
@[simp]
theorem nnnorm_one' {E : Type u_6} [seminormed_group E] :
theorem ne_one_of_nnnorm_ne_zero {E : Type u_6} [seminormed_group E] {a : E} :
theorem ne_zero_of_nnnorm_ne_zero {E : Type u_6} [seminormed_add_group E] {a : E} :
theorem nnnorm_mul_le' {E : Type u_6} [seminormed_group E] (a b : E) :
theorem nnnorm_add_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
@[simp]
theorem nnnorm_inv' {E : Type u_6} [seminormed_group E] (a : E) :
@[simp]
theorem nnnorm_neg {E : Type u_6} [seminormed_add_group E] (a : E) :
theorem nnnorm_sub_le {E : Type u_6} [seminormed_add_group E] (a b : E) :
theorem nnnorm_div_le {E : Type u_6} [seminormed_group E] (a b : E) :
theorem nnnorm_le_insert' {E : Type u_6} [seminormed_add_group E] (a b : E) :

Alias of nnnorm_le_nnnorm_add_nnnorm_sub'.

theorem mem_emetric_ball_one_iff {E : Type u_6} [seminormed_group E] {a : E} {r : ennreal} :
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‖₊) :
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‖₊) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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)
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)
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)
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)
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.

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.

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.

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.

theorem tendsto_norm_div_self {E : Type u_6} [seminormed_group E] (x : E) :
filter.tendsto (λ (a : E), a / x) (nhds x) (nhds 0)
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)
theorem tendsto_norm {E : Type u_6} [seminormed_add_group E] {x : E} :
filter.tendsto (λ (a : E), a) (nhds x) (nhds x)
theorem tendsto_norm' {E : Type u_6} [seminormed_group E] {x : E} :
filter.tendsto (λ (a : E), a) (nhds x) (nhds x)
theorem tendsto_norm_one {E : Type u_6} [seminormed_group E] :
filter.tendsto (λ (a : E), a) (nhds 1) (nhds 0)
theorem tendsto_norm_zero {E : Type u_6} [seminormed_add_group E] :
filter.tendsto (λ (a : E), a) (nhds 0) (nhds 0)
@[continuity]
theorem continuous_norm' {E : Type u_6} [seminormed_group E] :
continuous (λ (a : E), a)
@[continuity]
theorem continuous_norm {E : Type u_6} [seminormed_add_group E] :
continuous (λ (a : E), a)
@[continuity]
theorem continuous_nnnorm' {E : Type u_6} [seminormed_group E] :
continuous (λ (a : E), a‖₊)
@[continuity]
theorem continuous_nnnorm {E : Type u_6} [seminormed_add_group E] :
continuous (λ (a : E), a‖₊)
theorem mem_closure_one_iff_norm {E : Type u_6} [seminormed_group E] {x : E} :
theorem mem_closure_zero_iff_norm {E : Type u_6} [seminormed_add_group E] {x : E} :
theorem closure_one_eq {E : Type u_6} [seminormed_group E] :
closure {1} = {x : E | x = 0}
theorem closure_zero_eq {E : Type u_6} [seminormed_add_group E] :
closure {0} = {x : E | x = 0}
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 (•).

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 (•).

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 (•).

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 (•).

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)
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)
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‖₊)
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‖₊)
theorem continuous.norm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α E} :
continuous f continuous (λ (x : α), f x)
theorem continuous.norm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α E} :
continuous f continuous (λ (x : α), f x)
theorem continuous.nnnorm {α : Type u_3} {E : Type u_6} [seminormed_add_group E] [topological_space α] {f : α E} :
continuous f continuous (λ (x : α), f x‖₊)
theorem continuous.nnnorm' {α : Type u_3} {E : Type u_6} [seminormed_group E] [topological_space α] {f : α E} :
continuous f continuous (λ (x : α), f x‖₊)
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
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
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
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
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
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
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
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
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
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
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
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
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

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.

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 < ε)
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 < ε)
theorem norm_le_zero_iff' {E : Type u_6} [seminormed_add_group E] [t0_space E] {a : E} :
a 0 a = 0
theorem norm_le_zero_iff''' {E : Type u_6} [seminormed_group E] [t0_space E] {a : E} :
a 0 a = 1
theorem norm_eq_zero''' {E : Type u_6} [seminormed_group E] [t0_space E] {a : E} :
a = 0 a = 1
theorem norm_eq_zero' {E : Type u_6} [seminormed_add_group E] [t0_space E] {a : E} :
a = 0 a = 0
theorem norm_pos_iff' {E : Type u_6} [seminormed_add_group E] [t0_space E] {a : E} :
0 < a a 0
theorem norm_pos_iff''' {E : Type u_6} [seminormed_group E] [t0_space E] {a : E} :
0 < a a 1
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 < ε)
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 < ε)
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'
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'
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
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
@[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) :

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

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

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

Equations
theorem dist_inv {E : Type u_6} [seminormed_comm_group E] (x y : E) :
theorem dist_neg {E : Type u_6} [seminormed_add_comm_group E] (x y : E) :
@[simp]
theorem dist_self_add_right {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
@[simp]
theorem dist_self_mul_right {E : Type u_6} [seminormed_comm_group E] (a b : E) :
@[simp]
theorem dist_self_mul_left {E : Type u_6} [seminormed_comm_group E] (a b : E) :
@[simp]
theorem dist_self_add_left {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
@[simp]
theorem dist_self_sub_right {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
@[simp]
theorem dist_self_div_right {E : Type u_6} [seminormed_comm_group E] (a b : E) :
@[simp]
theorem dist_self_div_left {E : Type u_6} [seminormed_comm_group E] (a b : E) :
@[simp]
theorem dist_self_sub_left {E : Type u_6} [seminormed_add_comm_group E] (a b : E) :
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₂
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₂
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₂
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₂
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₂
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₂
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₂
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₂
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₂)
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₂)
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
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
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)
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)
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)
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)
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)
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)
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))
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))
theorem add_mem_ball_iff_norm {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : } :
theorem mul_mem_ball_iff_norm {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : } :
theorem mul_mem_closed_ball_iff_norm {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : } :
@[simp]
theorem preimage_add_ball {E : Type u_6} [seminormed_add_comm_group E] (a b : E) (r : ) :
@[simp]
theorem preimage_mul_ball {E : Type u_6} [seminormed_comm_group E] (a b : E) (r : ) :
@[simp]
theorem preimage_mul_sphere {E : Type u_6} [seminormed_comm_group E] (a b : E) (r : ) :
@[simp]
theorem preimage_add_sphere {E : Type u_6} [seminormed_add_comm_group E] (a b : E) (r : ) :
theorem norm_nsmul_le {E : Type u_6} [seminormed_add_comm_group E] (n : ) (a : E) :
theorem norm_pow_le_mul_norm {E : Type u_6} [seminormed_comm_group E] (n : ) (a : E) :
theorem nnnorm_pow_le_mul_norm {E : Type u_6} [seminormed_comm_group E] (n : ) (a : E) :
theorem nnnorm_nsmul_le {E : Type u_6} [seminormed_add_comm_group E] (n : ) (a : E) :
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)
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)
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)
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)
@[simp]
theorem add_mem_closed_ball_add_iff {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : } {c : E} :
@[simp]
theorem mul_mem_closed_ball_mul_iff {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : } {c : E} :
@[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
@[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
theorem smul_closed_ball'' {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : } :
theorem vadd_ball'' {E : Type u_6} [seminormed_add_comm_group E] {a b : E} {r : } :
theorem smul_ball'' {E : Type u_6} [seminormed_comm_group E] {a b : E} {r : } :
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
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
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
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
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₂
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₂
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₂
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₂
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‖₊)
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‖₊)
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)
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)
@[protected, instance]
Equations
@[simp]
theorem real.norm_eq_abs (r : ) :
theorem real.norm_of_nonneg {r : } (hr : 0 r) :
theorem real.norm_of_nonpos {r : } (hr : r 0) :
theorem real.le_norm_self (r : ) :
@[simp]
theorem real.norm_coe_nat (n : ) :
@[simp]
@[simp]
theorem real.norm_two  :
@[simp]
theorem real.nnnorm_two  :
theorem real.nnnorm_of_nonneg {r : } (hr : 0 r) :
r‖₊ = r, hr⟩
@[simp]
@[protected, instance]
Equations
@[norm_cast]
theorem int.norm_cast_real (m : ) :
theorem int.norm_eq_abs (n : ) :
@[simp]
theorem int.norm_coe_nat (n : ) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem rat.norm_cast_real (r : ) :
@[simp, norm_cast]
theorem int.norm_cast_rat (m : ) :
theorem norm_zsmul_le {α : Type u_3} [seminormed_add_comm_group α] (n : ) (a : α) :
theorem norm_zpow_le_mul_norm {α : Type u_3} [seminormed_comm_group α] (n : ) (a : α) :
theorem nnnorm_zsmul_le {α : Type u_3} [seminormed_add_comm_group α] (n : ) (a : α) :
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)⁻¹)
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)
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)
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)
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)
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)
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)
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)
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⁻¹) :
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⁻¹) :
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
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
@[protected, instance]

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

@[protected, instance]

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

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))
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))
@[simp]
theorem norm_eq_zero {E : Type u_6} [normed_add_group E] {a : E} :
a = 0 a = 0
@[simp]
theorem norm_eq_zero'' {E : Type u_6} [normed_group E] {a : E} :
a = 0 a = 1
theorem norm_ne_zero_iff' {E : Type u_6} [normed_group E] {a : E} :
a 0 a 1
theorem norm_ne_zero_iff {E : Type u_6} [normed_add_group E] {a : E} :
a 0 a 0
@[simp]
theorem norm_pos_iff {E : Type u_6} [normed_add_group E] {a : E} :
0 < a a 0
@[simp]
theorem norm_pos_iff'' {E : Type u_6} [normed_group E] {a : E} :
0 < a a 1
@[simp]
theorem norm_le_zero_iff'' {E : Type u_6} [normed_group E] {a : E} :
a 0 a = 1
@[simp]
theorem norm_le_zero_iff {E : Type u_6} [normed_add_group E] {a : E} :
a 0 a = 0
theorem norm_div_eq_zero_iff {E : Type u_6} [normed_group E] {a b : E} :
a / b = 0 a = b
theorem norm_sub_eq_zero_iff {E : Type u_6} [normed_add_group E] {a b : E} :
a - b = 0 a = b
theorem norm_sub_pos_iff {E : Type u_6} [normed_add_group E] {a b : E} :
0 < a - b a b
theorem norm_div_pos_iff {E : Type u_6} [normed_group E] {a b : E} :
0 < a / b a b
theorem eq_of_norm_sub_le_zero {E : Type u_6} [normed_add_group E] {a b : E} (h : a - b 0) :
a = b
theorem eq_of_norm_div_le_zero {E : Type u_6} [normed_group E] {a b : E} (h : a / b 0) :
a = b
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.

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.

@[simp]
theorem nnnorm_eq_zero' {E : Type u_6} [normed_group E] {a : E} :
a‖₊ = 0 a = 1
@[simp]
theorem nnnorm_eq_zero {E : Type u_6} [normed_add_group E] {a : E} :
a‖₊ = 0 a = 0
theorem nnnorm_ne_zero_iff' {E : Type u_6} [normed_group E] {a : E} :
theorem nnnorm_ne_zero_iff {E : Type u_6} [normed_add_group E] {a : E} :
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))
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))
def norm_group_norm (E : Type u_6) [normed_group E] :

The norm of a normed group as a group norm.

Equations

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

Equations

Some relations with has_compact_support

theorem has_compact_support_norm_iff {α : Type u_3} {E : Type u_6} [normed_add_group E] [topological_space α] {f : α E} :
theorem has_compact_support.norm {α : Type u_3} {E : Type u_6} [normed_add_group E] [topological_space α] {f : α E} :

Alias of the reverse direction of has_compact_support_norm_iff.

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
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
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 #

@[protected, instance]
def ulift.has_norm {E : Type u_6} [has_norm E] :
Equations
theorem ulift.norm_def {E : Type u_6} [has_norm E] (x : ulift E) :
@[simp]
theorem ulift.norm_up {E : Type u_6} [has_norm E] (x : E) :
@[simp]
theorem ulift.norm_down {E : Type u_6} [has_norm E] (x : ulift E) :
@[protected, instance]
def ulift.has_nnnorm {E : Type u_6} [has_nnnorm E] :
Equations
theorem ulift.nnnorm_def {E : Type u_6} [has_nnnorm E] (x : ulift E) :
@[simp]
theorem ulift.nnnorm_up {E : Type u_6} [has_nnnorm E] (x : E) :
@[simp]
theorem ulift.nnnorm_down {E : Type u_6} [has_nnnorm E] (x : ulift E) :

additive, multiplicative #

@[protected, instance]
def additive.has_norm {E : Type u_6} [has_norm E] :
Equations
@[protected, instance]
Equations
@[simp]
theorem norm_to_mul {E : Type u_6} [has_norm E] (x : additive E) :
@[simp]
theorem norm_of_mul {E : Type u_6} [has_norm E] (x : E) :
@[simp]
theorem norm_of_add {E : Type u_6} [has_norm E] (x : E) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem nnnorm_of_mul {E : Type u_6} [has_nnnorm E] (x : E) :
@[simp]

Order dual #

@[protected, instance]
Equations
@[simp]
theorem norm_to_dual {E : Type u_6} [has_norm E] (x : E) :
@[simp]
theorem norm_of_dual {E : Type u_6} [has_norm E] (x : Eᵒᵈ) :
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Binary product of normed groups #

@[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
theorem prod.norm_def {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] (x : E × F) :
theorem norm_fst_le {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] (x : E × F) :
theorem norm_snd_le {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] (x : E × F) :
theorem norm_prod_le_iff {E : Type u_6} {F : Type u_7} [has_norm E] [has_norm F] {x : E × F} {r : } :

Finite product of normed groups #

@[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
@[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
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‖₊))
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‖₊))
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‖₊)
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‖₊)
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.

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.

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
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
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
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
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.

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.

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
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
theorem norm_le_pi_norm {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) (i : ι) :
theorem norm_le_pi_norm' {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) (i : ι) :
theorem nnnorm_le_pi_nnnorm {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) (i : ι) :
theorem nnnorm_le_pi_nnnorm' {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) (i : ι) :
theorem pi_norm_const_le {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] (a : E) :
(λ (_x : ι), a) a
theorem pi_norm_const_le' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] (a : E) :
(λ (_x : ι), a) a
theorem pi_nnnorm_const_le' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] (a : E) :
(λ (_x : ι), a)‖₊ a‖₊
theorem pi_nnnorm_const_le {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] (a : E) :
(λ (_x : ι), a)‖₊ a‖₊
@[simp]
theorem pi_norm_const {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] [nonempty ι] (a : E) :
(λ (i : ι), a) = a
@[simp]
theorem pi_norm_const' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] [nonempty ι] (a : E) :
(λ (i : ι), a) = a
@[simp]
theorem pi_nnnorm_const' {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_group E] [nonempty ι] (a : E) :
(λ (i : ι), a)‖₊ = a‖₊
@[simp]
theorem pi_nnnorm_const {ι : Type u_4} {E : Type u_6} [fintype ι] [seminormed_add_group E] [nonempty ι] (a : E) :
(λ (i : ι), a)‖₊ = a‖₊
theorem pi.sum_norm_apply_le_norm' {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) :

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

theorem pi.sum_norm_apply_le_norm {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) :

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

theorem pi.sum_nnnorm_apply_le_nnnorm' {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_group (π i)] (f : Π (i : ι), π i) :

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

theorem pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_4} {π : ι Type u_9} [fintype ι] [Π (i : ι), seminormed_add_group (π i)] (f : Π (i : ι), π i) :

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

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

@[protected, instance]

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

Subgroups of normed groups #

@[protected, instance]

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

Equations
@[protected, instance]

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

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

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.

@[simp]
theorem add_subgroup.coe_norm {E : Type u_6} [seminormed_add_group E] {s : add_subgroup E} (x : s) :

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.

@[norm_cast]
theorem add_subgroup.norm_coe {E : Type u_6} [seminormed_add_group E] {s : add_subgroup E} (x : s) :

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.

@[norm_cast]
theorem subgroup.norm_coe {E : Type u_6} [seminormed_group E] {s : subgroup E} (x : s) :

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.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Submodules of normed groups #

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

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

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

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.

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

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.