# Normed (semi)groups #

In this file we define 10 classes:

• Norm, NNNorm: auxiliary classes endowing a type α with a function norm : α → ℝ (notation: ‖x‖) and nnnorm : α → ℝ≥0 (notation: ‖x‖₊), respectively;
• Seminormed...Group: A seminormed (additive) (commutative) group is an (additive) (commutative) group with a norm and a compatible pseudometric space structure: ∀ x y, dist x y = ‖x / y‖ or ∀ x y, dist x y = ‖x - y‖, depending on the group operation.
• Normed...Group: A normed (additive) (commutative) group is an (additive) (commutative) group with a norm and a compatible metric space structure.

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

## TODO #

This file is huge; move material into separate files, such as Mathlib/Analysis/Normed/Group/Lemmas.lean.

## 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 SeminormedGroup and SeminormedAddGroup not extend Group and AddGroup), but we choose not to for performance concerns.

## Tags #

normed group

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

• norm : E

the ℝ-valued norm function.

Instances
class NNNorm (E : Type u_9) :
Type u_9

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

• nnnorm : ENNReal

the ℝ≥0-valued norm function.

Instances

the ℝ-valued norm function.

Equations
• One or more equations did not get rendered due to their size.
Instances For

the ℝ≥0-valued norm function.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class SeminormedAddGroup (E : Type u_9) extends , , :
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.

• norm : E
• add_assoc : ∀ (a b c : E), a + b + c = a + (b + c)
• zero : E
• zero_add : ∀ (a : E), 0 + a = a
• add_zero : ∀ (a : E), a + 0 = a
• nsmul : EE
• nsmul_zero : ∀ (x : E), = 0
• nsmul_succ : ∀ (n : ) (x : E), AddMonoid.nsmul (n + 1) x = + x
• neg : EE
• sub : EEE
• sub_eq_add_neg : ∀ (a b : E), a - b = a + -b
• zsmul : EE
• zsmul_zero' : ∀ (a : E), = 0
• zsmul_succ' : ∀ (n : ) (a : E), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : E), = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : E), -a + a = 0
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : E), dist x y = x - y

The distance function is induced by the norm.

Instances
theorem SeminormedAddGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x - y

The distance function is induced by the norm.

class SeminormedGroup (E : Type u_9) extends , , :
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.

• norm : E
• mul : EEE
• mul_assoc : ∀ (a b c : E), a * b * c = a * (b * c)
• one : E
• one_mul : ∀ (a : E), 1 * a = a
• mul_one : ∀ (a : E), a * 1 = a
• npow : EE
• npow_zero : ∀ (x : E), = 1
• npow_succ : ∀ (n : ) (x : E), Monoid.npow (n + 1) x = * x
• inv : EE
• div : EEE
• div_eq_mul_inv : ∀ (a b : E), a / b = a * b⁻¹
• zpow : EE
• zpow_zero' : ∀ (a : E), = 1
• zpow_succ' : ∀ (n : ) (a : E), DivInvMonoid.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : E), = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel : ∀ (a : E), a⁻¹ * a = 1
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : E), dist x y = x / y

The distance function is induced by the norm.

Instances
theorem SeminormedGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x / y

The distance function is induced by the norm.

class NormedAddGroup (E : Type u_9) extends , , :
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.

• norm : E
• add_assoc : ∀ (a b c : E), a + b + c = a + (b + c)
• zero : E
• zero_add : ∀ (a : E), 0 + a = a
• add_zero : ∀ (a : E), a + 0 = a
• nsmul : EE
• nsmul_zero : ∀ (x : E), = 0
• nsmul_succ : ∀ (n : ) (x : E), AddMonoid.nsmul (n + 1) x = + x
• neg : EE
• sub : EEE
• sub_eq_add_neg : ∀ (a b : E), a - b = a + -b
• zsmul : EE
• zsmul_zero' : ∀ (a : E), = 0
• zsmul_succ' : ∀ (n : ) (a : E), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : E), = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : E), -a + a = 0
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : E}, dist x y = 0x = y
• dist_eq : ∀ (x y : E), dist x y = x - y

The distance function is induced by the norm.

Instances
theorem NormedAddGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x - y

The distance function is induced by the norm.

class NormedGroup (E : Type u_9) extends , , :
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.

• norm : E
• mul : EEE
• mul_assoc : ∀ (a b c : E), a * b * c = a * (b * c)
• one : E
• one_mul : ∀ (a : E), 1 * a = a
• mul_one : ∀ (a : E), a * 1 = a
• npow : EE
• npow_zero : ∀ (x : E), = 1
• npow_succ : ∀ (n : ) (x : E), Monoid.npow (n + 1) x = * x
• inv : EE
• div : EEE
• div_eq_mul_inv : ∀ (a b : E), a / b = a * b⁻¹
• zpow : EE
• zpow_zero' : ∀ (a : E), = 1
• zpow_succ' : ∀ (n : ) (a : E), DivInvMonoid.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : E), = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel : ∀ (a : E), a⁻¹ * a = 1
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : E}, dist x y = 0x = y
• dist_eq : ∀ (x y : E), dist x y = x / y

The distance function is induced by the norm.

Instances
theorem NormedGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x / y

The distance function is induced by the norm.

class SeminormedAddCommGroup (E : Type u_9) extends , , :
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.

• norm : E
• add_assoc : ∀ (a b c : E), a + b + c = a + (b + c)
• zero : E
• zero_add : ∀ (a : E), 0 + a = a
• add_zero : ∀ (a : E), a + 0 = a
• nsmul : EE
• nsmul_zero : ∀ (x : E), = 0
• nsmul_succ : ∀ (n : ) (x : E), AddMonoid.nsmul (n + 1) x = + x
• neg : EE
• sub : EEE
• sub_eq_add_neg : ∀ (a b : E), a - b = a + -b
• zsmul : EE
• zsmul_zero' : ∀ (a : E), = 0
• zsmul_succ' : ∀ (n : ) (a : E), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : E), = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : E), -a + a = 0
• add_comm : ∀ (a b : E), a + b = b + a
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : E), dist x y = x - y

The distance function is induced by the norm.

Instances
theorem SeminormedAddCommGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x - y

The distance function is induced by the norm.

class SeminormedCommGroup (E : Type u_9) extends , , :
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.

• norm : E
• mul : EEE
• mul_assoc : ∀ (a b c : E), a * b * c = a * (b * c)
• one : E
• one_mul : ∀ (a : E), 1 * a = a
• mul_one : ∀ (a : E), a * 1 = a
• npow : EE
• npow_zero : ∀ (x : E), = 1
• npow_succ : ∀ (n : ) (x : E), Monoid.npow (n + 1) x = * x
• inv : EE
• div : EEE
• div_eq_mul_inv : ∀ (a b : E), a / b = a * b⁻¹
• zpow : EE
• zpow_zero' : ∀ (a : E), = 1
• zpow_succ' : ∀ (n : ) (a : E), DivInvMonoid.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : E), = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel : ∀ (a : E), a⁻¹ * a = 1
• mul_comm : ∀ (a b : E), a * b = b * a
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : E), dist x y = x / y

The distance function is induced by the norm.

Instances
theorem SeminormedCommGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x / y

The distance function is induced by the norm.

class NormedAddCommGroup (E : Type u_9) extends , , :
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.

• norm : E
• add_assoc : ∀ (a b c : E), a + b + c = a + (b + c)
• zero : E
• zero_add : ∀ (a : E), 0 + a = a
• add_zero : ∀ (a : E), a + 0 = a
• nsmul : EE
• nsmul_zero : ∀ (x : E), = 0
• nsmul_succ : ∀ (n : ) (x : E), AddMonoid.nsmul (n + 1) x = + x
• neg : EE
• sub : EEE
• sub_eq_add_neg : ∀ (a b : E), a - b = a + -b
• zsmul : EE
• zsmul_zero' : ∀ (a : E), = 0
• zsmul_succ' : ∀ (n : ) (a : E), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : E), = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : E), -a + a = 0
• add_comm : ∀ (a b : E), a + b = b + a
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : E}, dist x y = 0x = y
• dist_eq : ∀ (x y : E), dist x y = x - y

The distance function is induced by the norm.

Instances
theorem NormedAddCommGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x - y

The distance function is induced by the norm.

class NormedCommGroup (E : Type u_9) extends , , :
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.

• norm : E
• mul : EEE
• mul_assoc : ∀ (a b c : E), a * b * c = a * (b * c)
• one : E
• one_mul : ∀ (a : E), 1 * a = a
• mul_one : ∀ (a : E), a * 1 = a
• npow : EE
• npow_zero : ∀ (x : E), = 1
• npow_succ : ∀ (n : ) (x : E), Monoid.npow (n + 1) x = * x
• inv : EE
• div : EEE
• div_eq_mul_inv : ∀ (a b : E), a / b = a * b⁻¹
• zpow : EE
• zpow_zero' : ∀ (a : E), = 1
• zpow_succ' : ∀ (n : ) (a : E), DivInvMonoid.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : E), = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel : ∀ (a : E), a⁻¹ * a = 1
• mul_comm : ∀ (a b : E), a * b = b * a
• dist : EE
• dist_self : ∀ (x : E), dist x x = 0
• dist_comm : ∀ (x y : E), dist x y = dist y x
• dist_triangle : ∀ (x y z : E), dist x z dist x y + dist y z
• edist : EEENNReal
• edist_dist : ∀ (x y : E), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set E | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : E}, dist x y = 0x = y
• dist_eq : ∀ (x y : E), dist x y = x / y

The distance function is induced by the norm.

Instances
theorem NormedCommGroup.dist_eq {E : Type u_9} [self : ] (x : E) (y : E) :
dist x y = x / y

The distance function is induced by the norm.

@[instance 100]
Equations
@[instance 100]
instance NormedGroup.toSeminormedGroup {E : Type u_6} [] :
Equations
• NormedGroup.toSeminormedGroup = let __src := inst;
@[instance 100]
Equations
@[instance 100]
Equations
• NormedCommGroup.toSeminormedCommGroup = let __src := inst;
@[instance 100]
Equations
@[instance 100]
Equations
• SeminormedCommGroup.toSeminormedGroup = let __src := inst;
@[instance 100]
Equations
@[instance 100]
instance NormedCommGroup.toNormedGroup {E : Type u_6} [] :
Equations
• NormedCommGroup.toNormedGroup = let __src := inst;
@[reducible, inline]
abbrev NormedAddGroup.ofSeparation {E : Type u_6} (h : ∀ (x : E), x = 0x = 0) :

Construct a NormedAddGroup from a SeminormedAddGroup satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedAddGroup instance as a special case of a more general SeminormedAddGroup instance.

Equations
Instances For
theorem NormedAddGroup.ofSeparation.proof_1 {E : Type u_1} (h : ∀ (x : E), x = 0x = 0) :
∀ {x y : E}, dist x y = 0x = y
@[reducible, inline]
abbrev NormedGroup.ofSeparation {E : Type u_6} [] (h : ∀ (x : E), x = 0x = 1) :

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

Equations
Instances For
theorem NormedAddCommGroup.ofSeparation.proof_1 {E : Type u_1} (h : ∀ (x : E), x = 0x = 0) :
∀ {x y : E}, dist x y = 0x = y
@[reducible, inline]
abbrev NormedAddCommGroup.ofSeparation {E : Type u_6} (h : ∀ (x : E), x = 0x = 0) :

Construct a NormedAddCommGroup from a SeminormedAddCommGroup satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedAddCommGroup instance as a special case of a more general SeminormedAddCommGroup instance.

Equations
• = let __src := inst; let __src_1 := ;
Instances For
@[reducible, inline]
abbrev NormedCommGroup.ofSeparation {E : Type u_6} (h : ∀ (x : E), x = 0x = 1) :

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

Equations
• = let __src := inst; let __src_1 := ;
Instances For
theorem SeminormedAddGroup.ofAddDist.proof_1 {E : Type u_1} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) (x : E) (y : E) :
dist x y = x - y
@[reducible, inline]
abbrev SeminormedAddGroup.ofAddDist {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

Construct a seminormed group from a translation-invariant distance.

Equations
Instances For
@[reducible, inline]
abbrev SeminormedGroup.ofMulDist {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

Construct a seminormed group from a multiplication-invariant distance.

Equations
Instances For
theorem SeminormedAddGroup.ofAddDist'.proof_1 {E : Type u_1} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) (x : E) (y : E) :
dist x y = x - y
@[reducible, inline]
abbrev SeminormedAddGroup.ofAddDist' {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
Instances For
@[reducible, inline]
abbrev SeminormedGroup.ofMulDist' {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
Instances For
@[reducible, inline]
abbrev SeminormedAddCommGroup.ofAddDist {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
theorem SeminormedAddCommGroup.ofAddDist.proof_1 {E : Type u_1} [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev SeminormedCommGroup.ofMulDist {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev SeminormedAddCommGroup.ofAddDist' {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

Construct a seminormed group from a translation-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
theorem SeminormedAddCommGroup.ofAddDist'.proof_1 {E : Type u_1} [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev SeminormedCommGroup.ofMulDist' {E : Type u_6} [Norm E] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedAddGroup.ofAddDist {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

Construct a normed group from a translation-invariant distance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedGroup.ofMulDist {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

Construct a normed group from a multiplication-invariant distance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedAddGroup.ofAddDist' {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

Construct a normed group from a translation-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedGroup.ofMulDist' {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedAddCommGroup.ofAddDist {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

Construct a normed group from a translation-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
theorem NormedAddCommGroup.ofAddDist.proof_1 {E : Type u_1} [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev NormedCommGroup.ofMulDist {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
theorem NormedAddCommGroup.ofAddDist'.proof_1 {E : Type u_1} [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev NormedAddCommGroup.ofAddDist' {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

Construct a normed group from a translation-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedCommGroup.ofMulDist' {E : Type u_6} [Norm E] [] [] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

Construct a normed group from a multiplication-invariant pseudodistance.

Equations
• = let __src := ;
Instances For
theorem AddGroupSeminorm.toSeminormedAddGroup.proof_8 {E : Type u_1} [] (f : ) (x : E) (y : E) :
dist x y = dist x y
theorem AddGroupSeminorm.toSeminormedAddGroup.proof_4 {E : Type u_1} [] (f : ) (x : E) (y : E) :
0 f (x - y)
theorem AddGroupSeminorm.toSeminormedAddGroup.proof_1 {E : Type u_1} [] (f : ) (x : E) :
f (x - x) = 0
@[reducible, inline]

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 UniformSpace instance on E).

Equations
Instances For
.sets = .sets
theorem AddGroupSeminorm.toSeminormedAddGroup.proof_3 {E : Type u_1} [] (f : ) (a : E) (b : E) (c : E) :
f (a - c) f (a - b) + f (b - c)
theorem AddGroupSeminorm.toSeminormedAddGroup.proof_5 {E : Type u_1} [] (f : ) (x : E) (y : E) :
f (x - y), = ENNReal.ofReal f (x - y),
theorem AddGroupSeminorm.toSeminormedAddGroup.proof_2 {E : Type u_1} [] (f : ) (x : E) (y : E) :
f (x - y) = f (y - x)
@[reducible, inline]
abbrev GroupSeminorm.toSeminormedGroup {E : Type u_6} [] (f : ) :

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 UniformSpace instance on E).

Equations
• f.toSeminormedGroup =
Instances For
@[reducible, inline]

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 UniformSpace instance on E).

Equations
Instances For
theorem AddGroupSeminorm.toSeminormedAddCommGroup.proof_1 {E : Type u_1} [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev GroupSeminorm.toSeminormedCommGroup {E : Type u_6} [] (f : ) :

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 UniformSpace instance on E).

Equations
• f.toSeminormedCommGroup = let __src := f.toSeminormedGroup;
Instances For
@[reducible, inline]

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 UniformSpace instance on E).

Equations
Instances For
∀ {x y : E}, dist x y = 0x = y
@[reducible, inline]
abbrev GroupNorm.toNormedGroup {E : Type u_6} [] (f : ) :

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 UniformSpace instance on E).

Equations
• f.toNormedGroup = let __src := f.toSeminormedGroup;
Instances For
theorem AddGroupNorm.toNormedAddCommGroup.proof_1 {E : Type u_1} [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]

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 UniformSpace instance on E).

Equations
Instances For
@[reducible, inline]
abbrev GroupNorm.toNormedCommGroup {E : Type u_6} [] (f : ) :

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 UniformSpace instance on E).

Equations
• f.toNormedCommGroup = let __src := f.toNormedGroup;
Instances For
theorem dist_eq_norm_sub {E : Type u_6} (a : E) (b : E) :
dist a b = a - b
theorem dist_eq_norm_div {E : Type u_6} [] (a : E) (b : E) :
dist a b = a / b
theorem dist_eq_norm_sub' {E : Type u_6} (a : E) (b : E) :
dist a b = b - a
theorem dist_eq_norm_div' {E : Type u_6} [] (a : E) (b : E) :
dist a b = b / a
theorem dist_eq_norm {E : Type u_6} (a : E) (b : E) :
dist a b = a - b

Alias of dist_eq_norm_sub.

theorem dist_eq_norm' {E : Type u_6} (a : E) (b : E) :
dist a b = b - a

Alias of dist_eq_norm_sub'.

theorem DiscreteTopology.of_forall_le_norm {E : Type u_6} {r : } (hpos : 0 < r) (hr : ∀ (x : E), x 0r x) :
theorem DiscreteTopology.of_forall_le_norm' {E : Type u_6} [] {r : } (hpos : 0 < r) (hr : ∀ (x : E), x 1r x) :
@[simp]
theorem dist_zero_right {E : Type u_6} (a : E) :
@[simp]
theorem dist_one_right {E : Type u_6} [] (a : E) :
theorem inseparable_zero_iff_norm {E : Type u_6} {a : E} :
theorem inseparable_one_iff_norm {E : Type u_6} [] {a : E} :
@[simp]
theorem dist_zero_left {E : Type u_6} :
dist 0 = norm
@[simp]
theorem dist_one_left {E : Type u_6} [] :
dist 1 = norm
theorem norm_sub_rev {E : Type u_6} (a : E) (b : E) :
a - b = b - a
theorem norm_div_rev {E : Type u_6} [] (a : E) (b : E) :
a / b = b / a
@[simp]
theorem norm_neg {E : Type u_6} (a : E) :
@[simp]
theorem norm_inv' {E : Type u_6} [] (a : E) :
theorem dist_indicator {α : Type u_3} {E : Type u_6} (s : Set α) (t : Set α) (f : αE) (x : α) :
dist (s.indicator f x) (t.indicator f x) = (symmDiff s t).indicator f x
theorem dist_mulIndicator {α : Type u_3} {E : Type u_6} [] (s : Set α) (t : Set α) (f : αE) (x : α) :
dist (s.mulIndicator f x) (t.mulIndicator f x) = (symmDiff s t).mulIndicator f x
theorem norm_add_le {E : Type u_6} (a : E) (b : E) :

Triangle inequality for the norm.

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

Triangle inequality for the norm.

theorem norm_add_le_of_le {E : Type u_6} {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
a₁ + a₂ r₁ + r₂
theorem norm_mul_le_of_le {E : Type u_6} [] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
a₁ * a₂ r₁ + r₂
theorem norm_add₃_le {E : Type u_6} (a : E) (b : E) (c : E) :
theorem norm_mul₃_le {E : Type u_6} [] (a : E) (b : E) (c : E) :
theorem norm_sub_le_norm_sub_add_norm_sub {E : Type u_6} (a : E) (b : E) (c : E) :
theorem norm_div_le_norm_div_add_norm_div {E : Type u_6} [] (a : E) (b : E) (c : E) :
@[simp]
theorem norm_nonneg {E : Type u_6} (a : E) :
@[simp]
theorem norm_nonneg' {E : Type u_6} [] (a : E) :
@[simp]
theorem abs_norm {E : Type u_6} (z : E) :
@[simp]
theorem abs_norm' {E : Type u_6} [] (z : E) :

Extension for the positivity tactic: multiplicative norms are nonnegative, via norm_nonneg'.

Instances For

Extension for the positivity tactic: additive norms are nonnegative, via norm_nonneg.

Instances For
@[simp]
theorem norm_zero {E : Type u_6} :
@[simp]
theorem norm_one' {E : Type u_6} [] :
theorem ne_zero_of_norm_ne_zero {E : Type u_6} {a : E} :
a 0a 0
theorem ne_one_of_norm_ne_zero {E : Type u_6} [] {a : E} :
a 0a 1
theorem norm_of_subsingleton {E : Type u_6} [] (a : E) :
theorem norm_of_subsingleton' {E : Type u_6} [] [] (a : E) :
theorem zero_lt_one_add_norm_sq {E : Type u_6} (x : E) :
0 < 1 + x ^ 2
theorem zero_lt_one_add_norm_sq' {E : Type u_6} [] (x : E) :
0 < 1 + x ^ 2
theorem norm_sub_le {E : Type u_6} (a : E) (b : E) :
theorem norm_div_le {E : Type u_6} [] (a : E) (b : E) :
theorem norm_sub_le_of_le {E : Type u_6} {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (H₁ : a₁ r₁) (H₂ : a₂ r₂) :
a₁ - a₂ r₁ + r₂
theorem norm_div_le_of_le {E : Type u_6} [] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (H₁ : a₁ r₁) (H₂ : a₂ r₂) :
a₁ / a₂ r₁ + r₂
theorem dist_le_norm_add_norm {E : Type u_6} (a : E) (b : E) :
theorem dist_le_norm_add_norm' {E : Type u_6} [] (a : E) (b : E) :
theorem abs_norm_sub_norm_le {E : Type u_6} (a : E) (b : E) :
theorem abs_norm_sub_norm_le' {E : Type u_6} [] (a : E) (b : E) :
theorem norm_sub_norm_le {E : Type u_6} (a : E) (b : E) :
theorem norm_sub_norm_le' {E : Type u_6} [] (a : E) (b : E) :
theorem dist_norm_norm_le {E : Type u_6} (a : E) (b : E) :
theorem dist_norm_norm_le' {E : Type u_6} [] (a : E) (b : E) :
theorem norm_le_norm_add_norm_sub' {E : Type u_6} (u : E) (v : E) :
theorem norm_le_norm_add_norm_div' {E : Type u_6} [] (u : E) (v : E) :
theorem norm_le_norm_add_norm_sub {E : Type u_6} (u : E) (v : E) :
theorem norm_le_norm_add_norm_div {E : Type u_6} [] (u : E) (v : E) :
theorem norm_le_insert' {E : Type u_6} (u : E) (v : E) :

Alias of norm_le_norm_add_norm_sub'.

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

Alias of norm_le_norm_add_norm_sub.

theorem norm_le_add_norm_add {E : Type u_6} (u : E) (v : E) :
theorem norm_le_mul_norm_add {E : Type u_6} [] (u : E) (v : E) :
theorem ball_eq {E : Type u_6} (y : E) (ε : ) :
= {x : E | x - y < ε}
theorem ball_eq' {E : Type u_6} [] (y : E) (ε : ) :
= {x : E | x / y < ε}
theorem ball_zero_eq {E : Type u_6} (r : ) :
= {x : E | x < r}
theorem ball_one_eq {E : Type u_6} [] (r : ) :
= {x : E | x < r}
theorem mem_ball_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
b b - a < r
theorem mem_ball_iff_norm'' {E : Type u_6} [] {a : E} {b : E} {r : } :
b b / a < r
theorem mem_ball_iff_norm' {E : Type u_6} {a : E} {b : E} {r : } :
b a - b < r
theorem mem_ball_iff_norm''' {E : Type u_6} [] {a : E} {b : E} {r : } :
b a / b < r
theorem mem_ball_zero_iff {E : Type u_6} {a : E} {r : } :
theorem mem_ball_one_iff {E : Type u_6} [] {a : E} {r : } :
theorem mem_closedBall_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
b b - a r
theorem mem_closedBall_iff_norm'' {E : Type u_6} [] {a : E} {b : E} {r : } :
b b / a r
theorem mem_closedBall_zero_iff {E : Type u_6} {a : E} {r : } :
theorem mem_closedBall_one_iff {E : Type u_6} [] {a : E} {r : } :
theorem mem_closedBall_iff_norm' {E : Type u_6} {a : E} {b : E} {r : } :
b a - b r
theorem mem_closedBall_iff_norm''' {E : Type u_6} [] {a : E} {b : E} {r : } :
b a / b r
theorem norm_le_of_mem_closedBall {E : Type u_6} {a : E} {b : E} {r : } (h : b ) :
theorem norm_le_of_mem_closedBall' {E : Type u_6} [] {a : E} {b : E} {r : } (h : b ) :
theorem norm_le_norm_add_const_of_dist_le {E : Type u_6} {a : E} {b : E} {r : } :
dist a b ra b + r
theorem norm_le_norm_add_const_of_dist_le' {E : Type u_6} [] {a : E} {b : E} {r : } :
dist a b ra b + r
theorem norm_lt_of_mem_ball {E : Type u_6} {a : E} {b : E} {r : } (h : b ) :
theorem norm_lt_of_mem_ball' {E : Type u_6} [] {a : E} {b : E} {r : } (h : b ) :
theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_6} (u : E) (v : E) (w : E) :
theorem norm_div_sub_norm_div_le_norm_div {E : Type u_6} [] (u : E) (v : E) (w : E) :
@[simp]
theorem mem_sphere_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
b b - a = r
@[simp]
theorem mem_sphere_iff_norm' {E : Type u_6} [] {a : E} {b : E} {r : } :
b b / a = r
theorem mem_sphere_zero_iff_norm {E : Type u_6} {a : E} {r : } :
theorem mem_sphere_one_iff_norm {E : Type u_6} [] {a : E} {r : } :
@[simp]
theorem norm_eq_of_mem_sphere {E : Type u_6} {r : } (x : (Metric.sphere 0 r)) :
x = r
@[simp]
theorem norm_eq_of_mem_sphere' {E : Type u_6} [] {r : } (x : (Metric.sphere 1 r)) :
x = r
theorem ne_zero_of_mem_sphere {E : Type u_6} {r : } (hr : r 0) (x : (Metric.sphere 0 r)) :
x 0
theorem ne_one_of_mem_sphere {E : Type u_6} [] {r : } (hr : r 0) (x : (Metric.sphere 1 r)) :
x 1
theorem ne_zero_of_mem_unit_sphere {E : Type u_6} (x : (Metric.sphere 0 1)) :
x 0
theorem ne_one_of_mem_unit_sphere {E : Type u_6} [] (x : (Metric.sphere 1 1)) :
x 1
def normAddGroupSeminorm (E : Type u_6) :

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

Equations
• = { toFun := norm, map_zero' := , add_le' := , neg' := }
Instances For
def normGroupSeminorm (E : Type u_6) [] :

The norm of a seminormed group as a group seminorm.

Equations
• = { toFun := norm, map_one' := , mul_le' := , inv' := }
Instances For
@[simp]
theorem coe_normAddGroupSeminorm (E : Type u_6) :
= norm
@[simp]
theorem coe_normGroupSeminorm (E : Type u_6) [] :
= norm
theorem NormedAddCommGroup.tendsto_nhds_zero {α : Type u_3} {E : Type u_6} {f : αE} {l : } :
Filter.Tendsto f l (nhds 0) ε > 0, ∀ᶠ (x : α) in l, f x < ε
theorem NormedCommGroup.tendsto_nhds_one {α : Type u_3} {E : Type u_6} [] {f : αE} {l : } :
Filter.Tendsto f l (nhds 1) ε > 0, ∀ᶠ (x : α) in l, f x < ε
theorem NormedAddCommGroup.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} {f : EF} {x : E} {y : F} :
Filter.Tendsto f (nhds x) (nhds y) ε > 0, δ > 0, ∀ (x' : E), x' - x < δf x' - y < ε
theorem NormedCommGroup.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [] [] {f : EF} {x : E} {y : F} :
Filter.Tendsto f (nhds x) (nhds y) ε > 0, δ > 0, ∀ (x' : E), x' / x < δf x' / y < ε
theorem NormedAddCommGroup.nhds_basis_norm_lt {E : Type u_6} (x : E) :
(nhds x).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y - x < ε}
theorem NormedCommGroup.nhds_basis_norm_lt {E : Type u_6} [] (x : E) :
(nhds x).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y / x < ε}
theorem NormedAddCommGroup.nhds_zero_basis_norm_lt {E : Type u_6} :
(nhds 0).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y < ε}
theorem NormedCommGroup.nhds_one_basis_norm_lt {E : Type u_6} [] :
(nhds 1).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y < ε}
theorem NormedAddCommGroup.uniformity_basis_dist {E : Type u_6} :
(uniformity E).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {p : E × E | p.1 - p.2 < ε}
theorem NormedCommGroup.uniformity_basis_dist {E : Type u_6} [] :
(uniformity E).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {p : E × E | p.1 / p.2 < ε}
@[instance 100]
instance SeminormedAddGroup.toNNNorm {E : Type u_6} :
Equations
• SeminormedAddGroup.toNNNorm = { nnnorm := fun (a : E) => a, }
@[instance 100]
instance SeminormedGroup.toNNNorm {E : Type u_6} [] :
Equations
• SeminormedGroup.toNNNorm = { nnnorm := fun (a : E) => a, }
@[simp]
theorem coe_nnnorm {E : Type u_6} (a : E) :
@[simp]
theorem coe_nnnorm' {E : Type u_6} [] (a : E) :
@[simp]
theorem coe_comp_nnnorm {E : Type u_6} :
NNReal.toReal nnnorm = norm
@[simp]
theorem coe_comp_nnnorm' {E : Type u_6} [] :
NNReal.toReal nnnorm = norm
theorem norm_toNNReal {E : Type u_6} {a : E} :
a.toNNReal = a‖₊
theorem norm_toNNReal' {E : Type u_6} [] {a : E} :
a.toNNReal = a‖₊
theorem nndist_eq_nnnorm_sub {E : Type u_6} (a : E) (b : E) :
theorem nndist_eq_nnnorm_div {E : Type u_6} [] (a : E) (b : E) :
theorem nndist_eq_nnnorm {E : Type u_6} (a : E) (b : E) :

Alias of nndist_eq_nnnorm_sub.

@[simp]
theorem nnnorm_zero {E : Type u_6} :
@[simp]
theorem nnnorm_one' {E : Type u_6} [] :
theorem ne_zero_of_nnnorm_ne_zero {E : Type u_6} {a : E} :
a‖₊ 0a 0
theorem ne_one_of_nnnorm_ne_zero {E : Type u_6} [] {a : E} :
a‖₊ 0a 1
theorem nnnorm_add_le {E : Type u_6} (a : E) (b : E) :
theorem nnnorm_mul_le' {E : Type u_6} [] (a : E) (b : E) :
@[simp]
theorem nnnorm_neg {E : Type u_6} (a : E) :
@[simp]
theorem nnnorm_inv' {E : Type u_6} [] (a : E) :
theorem nndist_indicator {α : Type u_3} {E : Type u_6} (s : Set α) (t : Set α) (f : αE) (x : α) :
nndist (s.indicator f x) (t.indicator f x) = (symmDiff s t).indicator f x‖₊
theorem nndist_mulIndicator {α : Type u_3} {E : Type u_6} [] (s : Set α) (t : Set α) (f : αE) (x : α) :
nndist (s.mulIndicator f x) (t.mulIndicator f x) = (symmDiff s t).mulIndicator f x‖₊
theorem nnnorm_sub_le {E : Type u_6} (a : E) (b : E) :
theorem nnnorm_div_le {E : Type u_6} [] (a : E) (b : E) :
theorem nndist_nnnorm_nnnorm_le {E : Type u_6} (a : E) (b : E) :
theorem nndist_nnnorm_nnnorm_le' {E : Type u_6} [] (a : E) (b : E) :
theorem nnnorm_le_nnnorm_add_nnnorm_div {E : Type u_6} [] (a : E) (b : E) :
theorem nnnorm_le_nnnorm_add_nnnorm_div' {E : Type u_6} [] (a : E) (b : E) :
theorem nnnorm_le_insert' {E : Type u_6} (a : E) (b : E) :

Alias of nnnorm_le_nnnorm_add_nnnorm_sub'.

theorem nnnorm_le_insert {E : Type u_6} (a : E) (b : E) :

Alias of nnnorm_le_nnnorm_add_nnnorm_sub.

theorem nnnorm_le_add_nnnorm_add {E : Type u_6} (a : E) (b : E) :
theorem nnnorm_le_mul_nnnorm_add {E : Type u_6} [] (a : E) (b : E) :
theorem ofReal_norm_eq_coe_nnnorm {E : Type u_6} (a : E) :
theorem ofReal_norm_eq_coe_nnnorm' {E : Type u_6} [] (a : E) :
theorem toReal_coe_nnnorm {E : Type u_6} (a : E) :
(↑a‖₊).toReal = a

The non negative norm seen as an ENNReal and then as a Real is equal to the norm.

theorem toReal_coe_nnnorm' {E : Type u_6} [] (a : E) :
(↑a‖₊).toReal = a

The non negative norm seen as an ENNReal and then as a Real is equal to the norm.

theorem edist_eq_coe_nnnorm_sub {E : Type u_6} (a : E) (b : E) :
edist a b = a - b‖₊
theorem edist_eq_coe_nnnorm_div {E : Type u_6} [] (a : E) (b : E) :
edist a b = a / b‖₊
theorem edist_eq_coe_nnnorm {E : Type u_6} (x : E) :
edist x 0 = x‖₊
theorem edist_eq_coe_nnnorm' {E : Type u_6} [] (x : E) :
edist x 1 = x‖₊
theorem edist_indicator {α : Type u_3} {E : Type u_6} (s : Set α) (t : Set α) (f : αE) (x : α) :
edist (s.indicator f x) (t.indicator f x) = (symmDiff s t).indicator f x‖₊
theorem edist_mulIndicator {α : Type u_3} {E : Type u_6} [] (s : Set α) (t : Set α) (f : αE) (x : α) :
edist (s.mulIndicator f x) (t.mulIndicator f x) = (symmDiff s t).mulIndicator f x‖₊
theorem mem_emetric_ball_zero_iff {E : Type u_6} {a : E} {r : ENNReal} :
a a‖₊ < r
theorem mem_emetric_ball_one_iff {E : Type u_6} [] {a : E} {r : ENNReal} :
a a‖₊ < r
theorem tendsto_iff_norm_sub_tendsto_zero {α : Type u_3} {E : Type u_6} {f : αE} {a : } {b : E} :
Filter.Tendsto f a (nhds b) Filter.Tendsto (fun (e : α) => f e - b) a (nhds 0)
theorem tendsto_iff_norm_div_tendsto_zero {α : Type u_3} {E : Type u_6} [] {f : αE} {a : } {b : E} :
Filter.Tendsto f a (nhds b) Filter.Tendsto (fun (e : α) => f e / b) a (nhds 0)
theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} {f : αE} {a : } :
Filter.Tendsto f a (nhds 0) Filter.Tendsto (fun (x : α) => f x) a (nhds 0)
theorem tendsto_one_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} [] {f : αE} {a : } :
Filter.Tendsto f a (nhds 1) Filter.Tendsto (fun (x : α) => f x) a (nhds 0)
theorem comap_norm_nhds_zero {E : Type u_6} :
Filter.comap norm (nhds 0) = nhds 0
theorem comap_norm_nhds_one {E : Type u_6} [] :
Filter.comap norm (nhds 0) = nhds 1
theorem squeeze_zero_norm' {α : Type u_3} {E : Type u_6} {f : αE} {a : α} {t₀ : } (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 0. In this pair of lemmas (squeeze_zero_norm' and squeeze_zero_norm), following a convention of similar lemmas in Topology.MetricSpace.Pseudo.Defs and Topology.Algebra.Order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

theorem squeeze_one_norm' {α : Type u_3} {E : Type u_6} [] {f : αE} {a : α} {t₀ : } (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 (neutral element of SeminormedGroup). In this pair of lemmas (squeeze_one_norm' and squeeze_one_norm), following a convention of similar lemmas in Topology.MetricSpace.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} {f : αE} {a : α} {t₀ : } (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} [] {f : αE} {a : α} {t₀ : } (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_sub_self {E : Type u_6} (x : E) :
Filter.Tendsto (fun (a : E) => a - x) (nhds x) (nhds 0)
theorem tendsto_norm_div_self {E : Type u_6} [] (x : E) :
Filter.Tendsto (fun (a : E) => a / x) (nhds x) (nhds 0)
theorem tendsto_norm {E : Type u_6} {x : E} :
Filter.Tendsto (fun (a : E) => a) (nhds x) (nhds x)
theorem tendsto_norm' {E : Type u_6} [] {x : E} :
Filter.Tendsto (fun (a : E) => a) (nhds x) (nhds x)
theorem tendsto_norm_zero {E : Type u_6} :
Filter.Tendsto (fun (a : E) => a) (nhds 0) (nhds 0)
theorem tendsto_norm_one {E : Type u_6} [] :
Filter.Tendsto (fun (a : E) => a) (nhds 1) (nhds 0)
theorem continuous_norm {E : Type u_6} :
Continuous fun (a : E) => a
theorem continuous_norm' {E : Type u_6} [] :
Continuous fun (a : E) => a
theorem continuous_nnnorm {E : Type u_6} :
Continuous fun (a : E) => a‖₊
theorem continuous_nnnorm' {E : Type u_6} [] :
Continuous fun (a : E) => a‖₊
theorem mem_closure_zero_iff_norm {E : Type u_6} {x : E} :
theorem mem_closure_one_iff_norm {E : Type u_6} [] {x : E} :
theorem closure_zero_eq {E : Type u_6} :
closure {0} = {x : E | x = 0}
theorem closure_one_eq {E : Type u_6} [] :
closure {1} = {x : E | x = 0}
theorem Filter.Tendsto.norm {α : Type u_3} {E : Type u_6} {a : E} {l : } {f : αE} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (x : α) => f x) l (nhds a)
theorem Filter.Tendsto.norm' {α : Type u_3} {E : Type u_6} [] {a : E} {l : } {f : αE} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (x : α) => f x) l (nhds a)
theorem Filter.Tendsto.nnnorm {α : Type u_3} {E : Type u_6} {a : E} {l : } {f : αE} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (x : α) => f x‖₊) l (nhds a‖₊)
theorem Filter.Tendsto.nnnorm' {α : Type u_3} {E : Type u_6} [] {a : E} {l : } {f : αE} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (x : α) => f x‖₊) l (nhds a‖₊)
theorem Continuous.norm {α : Type u_3} {E : Type u_6} [] {f : αE} :
Continuous fun (x : α) => f x
theorem Continuous.norm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} :
Continuous fun (x : α) => f x
theorem Continuous.nnnorm {α : Type u_3} {E : Type u_6} [] {f : αE} :
Continuous fun (x : α) => f x‖₊
theorem Continuous.nnnorm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} :
Continuous fun (x : α) => f x‖₊
theorem ContinuousAt.norm {α : Type u_3} {E : Type u_6} [] {f : αE} {a : α} (h : ) :
ContinuousAt (fun (x : α) => f x) a
theorem ContinuousAt.norm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} {a : α} (h : ) :
ContinuousAt (fun (x : α) => f x) a
theorem ContinuousAt.nnnorm {α : Type u_3} {E : Type u_6} [] {f : αE} {a : α} (h : ) :
ContinuousAt (fun (x : α) => f x‖₊) a
theorem ContinuousAt.nnnorm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} {a : α} (h : ) :
ContinuousAt (fun (x : α) => f x‖₊) a
theorem ContinuousWithinAt.norm {α : Type u_3} {E : Type u_6} [] {f : αE} {s : Set α} {a : α} (h : ) :
ContinuousWithinAt (fun (x : α) => f x) s a
theorem ContinuousWithinAt.norm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} {s : Set α} {a : α} (h : ) :
ContinuousWithinAt (fun (x : α) => f x) s a
theorem ContinuousWithinAt.nnnorm {α : Type u_3} {E : Type u_6} [] {f : αE} {s : Set α} {a : α} (h : ) :
ContinuousWithinAt (fun (x : α) => f x‖₊) s a
theorem ContinuousWithinAt.nnnorm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} {s : Set α} {a : α} (h : ) :
ContinuousWithinAt (fun (x : α) => f x‖₊) s a
theorem ContinuousOn.norm {α : Type u_3} {E : Type u_6} [] {f : αE} {s : Set α} (h : ) :
ContinuousOn (fun (x : α) => f x) s
theorem ContinuousOn.norm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} {s : Set α} (h : ) :
ContinuousOn (fun (x : α) => f x) s
theorem ContinuousOn.nnnorm {α : Type u_3} {E : Type u_6} [] {f : αE} {s : Set α} (h : ) :
ContinuousOn (fun (x : α) => f x‖₊) s
theorem ContinuousOn.nnnorm' {α : Type u_3} {E : Type u_6} [] [] {f : αE} {s : Set α} (h : ) :
ContinuousOn (fun (x : α) => f x‖₊) s
theorem eventually_ne_of_tendsto_norm_atTop {α : Type u_3} {E : Type u_6} {l : } {f : αE} (h : Filter.Tendsto (fun (y : α) => f y) l Filter.atTop) (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_atTop' {α : Type u_3} {E : Type u_6} [] {l : } {f : αE} (h : Filter.Tendsto (fun (y : α) => f y) l Filter.atTop) (x : E) :
∀ᶠ (y : α) in l, f y x

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

theorem SeminormedAddCommGroup.mem_closure_iff {E : Type u_6} {s : Set E} {a : E} :
a ∀ (ε : ), 0 < εbs, a - b < ε
theorem SeminormedCommGroup.mem_closure_iff {E : Type u_6} [] {s : Set E} {a : E} :
a ∀ (ε : ), 0 < εbs, a / b < ε
theorem norm_le_zero_iff' {E : Type u_6} [] {a : E} :
a 0 a = 0
theorem norm_le_zero_iff''' {E : Type u_6} [] [] {a : E} :
a 0 a = 1
theorem norm_eq_zero' {E : Type u_6} [] {a : E} :
a = 0 a = 0
theorem norm_eq_zero''' {E : Type u_6} [] [] {a : E} :
a = 0 a = 1
theorem norm_pos_iff' {E : Type u_6} [] {a : E} :
0 < a a 0
theorem norm_pos_iff''' {E : Type u_6} [] [] {a : E} :
0 < a a 1
theorem SeminormedAddGroup.tendstoUniformlyOn_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} {f : ικG} {s : Set κ} {l : } :
ε > 0, ∀ᶠ (i : ι) in l, xs, f i x < ε
theorem SeminormedGroup.tendstoUniformlyOn_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [] {f : ικG} {s : Set κ} {l : } :
ε > 0, ∀ᶠ (i : ι) in l, xs, f i x < ε
theorem SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} {f : ικG} {l : } {l' : } :
TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) l'
theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [] {f : ικG} {l : } {l' : } :
TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
theorem SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} {f : ικG} {s : Set κ} {l : } :
TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) s
theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [] {f : ικG} {s : Set κ} {l : } :
TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) s
@[reducible, inline]
abbrev SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] (f : 𝓕) :

A group homomorphism from an AddGroup to a SeminormedAddGroup induces a SeminormedAddGroup structure on the domain.

Equations
Instances For
theorem SeminormedAddGroup.induced.proof_1 {𝓕 : Type u_3} (E : Type u_1) (F : Type u_2) [FunLike 𝓕 E F] [] [] (f : 𝓕) (x : E) (y : E) :
dist x y = x - y
@[reducible, inline]
abbrev SeminormedGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] [] (f : 𝓕) :

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

Equations
Instances For
theorem SeminormedAddCommGroup.induced.proof_1 (E : Type u_1) [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev SeminormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] (f : 𝓕) :

A group homomorphism from an AddCommGroup to a SeminormedAddGroup induces a SeminormedAddCommGroup structure on the domain.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev SeminormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] [] (f : 𝓕) :

A group homomorphism from a CommGroup to a SeminormedGroup induces a SeminormedCommGroup structure on the domain.

Equations
• = let __src := ;
Instances For
@[reducible, inline]
abbrev NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] [] (f : 𝓕) (h : ) :

An injective group homomorphism from an AddGroup to a NormedAddGroup induces a NormedAddGroup structure on the domain.

Equations
Instances For
@[reducible, inline]
abbrev NormedGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] [] (f : 𝓕) (h : ) :

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

Equations
Instances For
theorem NormedAddCommGroup.induced.proof_1 (E : Type u_1) [] (a : E) (b : E) :
a + b = b + a
@[reducible, inline]
abbrev NormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] [] (f : 𝓕) (h : ) :

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

Equations
Instances For
@[reducible, inline]
abbrev NormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [] [] [] (f : 𝓕) (h : ) :

An injective group homomorphism from a CommGroup to a NormedGroup induces a NormedCommGroup structure on the domain.

Equations
Instances For
theorem dist_neg {E : Type u_6} (x : E) (y : E) :
dist (-x) y = dist x (-y)
theorem dist_inv {E : Type u_6} (x : E) (y : E) :
theorem norm_multiset_sum_le {E : Type u_9} (m : ) :
m.sum (Multiset.map (fun (x : E) => x) m).sum
theorem norm_multiset_prod_le {E : Type u_6} (m : ) :
m.prod (Multiset.map (fun (x : E) => x) m).sum
theorem norm_sum_le {ι : Type u_9} {E : Type u_10} (s : ) (f : ιE) :
is, f i is, f i
theorem norm_prod_le {ι : Type u_4} {E : Type u_6} (s : ) (f : ιE) :
is, f i is, f i
theorem norm_sum_le_of_le {ι : Type u_4} {E : Type u_6} (s : ) {f : ιE} {n : ι} (h : bs, f b n b) :
bs, f b bs, n b
theorem norm_prod_le_of_le {ι : Type u_4} {E : Type u_6} (s : ) {f : ιE} {n : ι} (h : bs, f b n b) :
bs, f b bs, n b
theorem dist_sum_sum_le_of_le {ι : Type u_4} {E : Type u_6} (s : ) {f : ιE} {a : ιE} {d : ι} (h : bs, dist (f b) (a b) d b) :
dist (∑ bs, f b) (∑ bs, a b) bs, d b
theorem dist_prod_prod_le_of_le {ι : Type u_4} {E : Type u_6} (s : ) {f : ιE} {a : ιE} {d : ι} (h : bs, dist (f b) (a b) d b) :
dist (∏ bs, f b) (∏ bs, a b) bs, d b
theorem dist_sum_sum_le {ι : Type u_4} {E : Type u_6} (s : ) (f : ιE) (a : ιE) :
dist (∑ bs, f b) (∑ bs, a b) bs, dist (f b) (a b)
theorem dist_prod_prod_le {ι : Type u_4} {E : Type u_6} (s : ) (f : ιE) (a : ιE) :
dist (∏ bs, f b) (∏ bs, a b) bs, dist (f b) (a b)
theorem add_mem_ball_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
a + b b < r
theorem mul_mem_ball_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
a * b b < r
theorem add_mem_closedBall_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
a + b b r
theorem mul_mem_closedBall_iff_norm {E : Type u_6} {a : E} {b : E} {r : } :
a * b b r
@[simp]
theorem preimage_add_ball {E : Type u_6} (a : E) (b : E) (r : ) :
(fun (x : E) => b + x) ⁻¹' = Metric.ball (a - b) r
@[simp]
theorem preimage_mul_ball {E : Type u_6} (a : E) (b : E) (r : ) :
(fun (x : E) => b * x) ⁻¹' = Metric.ball (a / b) r
@[simp]
theorem preimage_add_closedBall {E : Type u_6} (a : E) (b : E) (r : ) :
(fun (x : E) => b + x) ⁻¹' = Metric.closedBall (a - b) r
@[simp]
theorem preimage_mul_closedBall {E : Type u_6} (a : E) (b : E) (r : ) :
(fun (x : E) => b * x) ⁻¹' = Metric.closedBall (a / b) r
@[simp]
theorem preimage_add_sphere {E : Type u_6} (a : E) (b : E) (r : ) :
(fun (x : E) => b + x) ⁻¹' = Metric.sphere (a - b) r
@[simp]
theorem preimage_mul_sphere {E : Type u_6} (a : E) (b : E) (r : ) :
(fun (x : E) => b * x) ⁻¹' = Metric.sphere (a / b) r
theorem norm_nsmul_le {E : Type u_6} (n : ) (a : E) :
n a n * a
theorem norm_pow_le_mul_norm {E : Type u_6} (n : ) (a : E) :
a ^ n n * a
theorem nnnorm_nsmul_le {E : Type u_6} (n : ) (a : E) :
theorem nnnorm_pow_le_mul_norm {E : Type u_6} (n : ) (a : E) :
theorem nsmul_mem_closedBall {E : Type u_6} {a : E} {b : E} {r : } {n : } (h : a ) :
n a Metric.closedBall (n b) (n r)
theorem pow_mem_closedBall {E : Type u_6} {a : E} {b : E} {r : } {n : } (h : a ) :
a ^ n Metric.closedBall (b ^ n) (n r)
theorem nsmul_mem_ball {E : Type u_6} {a : E} {b : E} {r : } {n : } (hn : 0 < n) (h : a ) :
n a Metric.ball (n b) (n r)
theorem pow_mem_ball {E : Type u_6} {a : E} {b : E} {r : } {n : } (hn : 0 < n) (h : a ) :
a ^ n Metric.ball (b ^ n) (n r)
theorem add_mem_closedBall_add_iff {E : Type u_6} {a : E} {b : E} {r : } {c : E} :
a + c Metric.closedBall (b + c) r a
theorem mul_mem_closedBall_mul_iff {E : Type u_6} {a : E} {b : E} {r : } {c : E} :
a * c Metric.closedBall (b * c) r a
theorem add_mem_ball_add_iff {E : Type u_6} {a : E} {b : E} {r : } {c : E} :
a + c Metric.ball (b + c) r a
theorem mul_mem_ball_mul_iff {E : Type u_6} {a : E} {b : E} {r : } {c : E} :
a * c Metric.ball (b * c) r a
theorem vadd_closedBall'' {E : Type u_6} {a : E} {b : E} {r : } :
theorem smul_closedBall'' {E : Type u_6} {a : E} {b : E} {r : } :
theorem vadd_ball'' {E : Type u_6} {a : E} {b : E} {r : } :
theorem smul_ball'' {E : Type u_6} {a : E} {b : E} {r : } :
a = Metric.ball (a b) r
theorem controlled_sum_of_mem_closure {E : Type u_6} {a : E} {s : } (hg : a closure s) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (v : E), Filter.Tendsto (fun (n : ) => iFinset.range (n + 1), v i) Filter.atTop (nhds a) (∀ (n : ), v n s) v 0 - a < b 0 ∀ (n : ), 0 < nv n < b n
theorem controlled_prod_of_mem_closure {E : Type u_6} {a : E} {s : } (hg : a closure s) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (v : E), Filter.Tendsto (fun (n : ) => iFinset.range (n + 1), v i) Filter.atTop (nhds a) (∀ (n : ), v n s) v 0 / a < b 0 ∀ (n : ), 0 < nv n < b n
theorem controlled_sum_of_mem_closure_range {E : Type u_6} {F : Type u_7} {j : E →+ F} {b : F} (hb : b closure j.range) {f : } (b_pos : ∀ (n : ), 0 < f n) :
∃ (a : E), Filter.Tendsto (fun (n : ) => iFinset.range (n + 1), j (a i)) Filter.atTop (nhds b) j (a 0) - b < f 0 ∀ (n : ), 0 < nj (a n) < f n
theorem controlled_prod_of_mem_closure_range {E : Type u_6} {F : Type u_7} {j : E →* F} {b : F} (hb : b closure j.range) {f : } (b_pos : ∀ (n : ), 0 < f n) :
∃ (a : E), Filter.Tendsto (fun (n : ) => iFinset.range (n + 1), j (a i)) Filter.atTop (nhds b) j (a 0) / b < f 0 ∀ (n : ), 0 < nj (a n) < f n
theorem nnnorm_multiset_sum_le {E : Type u_6} (m : ) :
m.sum‖₊ (Multiset.map (fun (x : E) => x‖₊) m).sum
theorem nnnorm_multiset_prod_le {E : Type u_6} (m : ) :
m.prod‖₊ (Multiset.map (fun (x : E) => x‖₊) m).sum
theorem nnnorm_sum_le {ι : Type u_4} {E : Type u_6} (s : ) (f : ιE) :
as, f a‖₊ as, f a‖₊
theorem nnnorm_prod_le {ι : Type u_4} {E : Type u_6} (s : ) (f : ιE) :
as, f a‖₊ as, f a‖₊
theorem nnnorm_sum_le_of_le {ι : Type u_4} {E : Type u_6} (s : ) {f : ιE} {n : ιNNReal} (h : bs, f b‖₊ n b) :
bs, f b‖₊ bs, n b
theorem nnnorm_prod_le_of_le {ι : Type u_4} {E : Type u_6} (s : ) {f : ιE} {n : ιNNReal} (h : bs, f b‖₊ n b) :
bs, f b‖₊ bs, n b
instance Real.norm :
Equations
@[simp]
theorem Real.norm_eq_abs (r : ) :
r = |r|
theorem Real.norm_of_nonneg {r : } (hr : 0 r) :
theorem Real.norm_of_nonpos {r : } (hr : r 0) :
theorem Real.norm_natCast (n : ) :
n = n
@[simp]
theorem Real.nnnorm_natCast (n : ) :
n‖₊ = n
@[deprecated Real.norm_natCast]
theorem Real.norm_coe_nat (n : ) :
n = n

Alias of Real.norm_natCast.

@[deprecated Real.nnnorm_natCast]
theorem Real.nnnorm_coe_nat (n : ) :
n‖₊ = n

Alias of Real.nnnorm_natCast.

@[simp]
theorem Real.nnnorm_of_nonneg {r : } (hr : 0 r) :
r‖₊ = r, hr
@[simp]
theorem Real.ennnorm_eq_ofReal {r : } (hr : 0 r) :
theorem Real.toNNReal_eq_nnnorm_of_nonneg {r : } (hr : 0 r) :
r.toNNReal = r‖₊
Equations
@[simp]
@[simp]
theorem norm_eq_zero {E : Type u_6} [] {a : E} :
a = 0 a = 0
@[simp]
theorem norm_eq_zero'' {E : Type u_6} [] {a : E} :
a = 0 a = 1
theorem norm_ne_zero_iff {E : Type u_6} [] {a : E} :
a 0 a 0
theorem norm_ne_zero_iff' {E : Type u_6} [] {a : E} :
a 0 a 1
@[simp]
theorem norm_pos_iff {E : Type u_6} [] {a : E} :
0 < a a 0
@[simp]
theorem norm_pos_iff'' {E : Type u_6} [] {a : E} :
0 < a a 1
@[simp]
theorem norm_le_zero_iff {E : Type u_6} [] {a : E} :
a 0 a = 0
@[simp]
theorem norm_le_zero_iff'' {E : Type u_6} [] {a : E} :
a 0 a = 1
theorem norm_sub_eq_zero_iff {E : Type u_6} [] {a : E} {b : E} :
a - b = 0 a = b
theorem norm_div_eq_zero_iff {E : Type u_6} [] {a : E} {b : E} :
a / b = 0 a = b
theorem norm_sub_pos_iff {E : Type u_6} [] {a : E} {b : E} :
0 < a - b a b
theorem norm_div_pos_iff {E : Type u_6} [] {a : E} {b : E} :
0 < a / b a b
theorem eq_of_norm_sub_le_zero {E : Type u_6} [] {a : E} {b : E} (h : a - b 0) :
a = b
theorem eq_of_norm_div_le_zero {E : Type u_6} [] {a : E} {b : E} (h : a / b 0) :
a = b
theorem eq_of_norm_div_eq_zero {E : Type u_6} [] {a : E} {b : E} :
a / b = 0a = b

Alias of the forward direction of norm_div_eq_zero_iff.

theorem eq_of_norm_sub_eq_zero {E : Type u_6} [] {a : E} {b : E} :
a - b