mathlib documentation

analysis.normed.group.basic

Normed (semi)groups #

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_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
@[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_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_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
@[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 dist_le_norm_mul_norm {E : Type u_6} [seminormed_group E] (a b : E) :
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 monoid_hom_class.bound_of_antilipschitz {𝓕 : 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 : antilipschitz_with K f) (x : E) :
theorem add_monoid_hom_class.bound_of_antilipschitz {𝓕 : 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 : 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} [