Normed (semi)groups #
In this file we define 10 classes:
Norm
,NNNorm
: auxiliary classes endowing a typeα
with a functionnorm : α → ℝ
(notation:‖x‖
) andnnnorm : α → ℝ≥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
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
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 : E → E → E
- zero : E
- nsmul : ℕ → E → E
- nsmul_zero : ∀ (x : E), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : E), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : E → E
- sub : E → E → E
- zsmul : ℤ → E → E
- zsmul_zero' : ∀ (a : E), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- one : E
- npow : ℕ → E → E
- npow_zero : ∀ (x : E), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : E), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : E → E
- div : E → E → E
- zpow : ℤ → E → E
- zpow_zero' : ∀ (a : E), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- zero : E
- nsmul : ℕ → E → E
- nsmul_zero : ∀ (x : E), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : E), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : E → E
- sub : E → E → E
- zsmul : ℤ → E → E
- zsmul_zero' : ∀ (a : E), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- one : E
- npow : ℕ → E → E
- npow_zero : ∀ (x : E), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : E), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : E → E
- div : E → E → E
- zpow : ℤ → E → E
- zpow_zero' : ∀ (a : E), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- zero : E
- nsmul : ℕ → E → E
- nsmul_zero : ∀ (x : E), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : E), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : E → E
- sub : E → E → E
- zsmul : ℤ → E → E
- zsmul_zero' : ∀ (a : E), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- one : E
- npow : ℕ → E → E
- npow_zero : ∀ (x : E), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : E), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : E → E
- div : E → E → E
- zpow : ℤ → E → E
- zpow_zero' : ∀ (a : E), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- zero : E
- nsmul : ℕ → E → E
- nsmul_zero : ∀ (x : E), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : E), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : E → E
- sub : E → E → E
- zsmul : ℤ → E → E
- zsmul_zero' : ∀ (a : E), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
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 : E → E → E
- one : E
- npow : ℕ → E → E
- npow_zero : ∀ (x : E), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : E), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : E → E
- div : E → E → E
- zpow : ℤ → E → E
- zpow_zero' : ∀ (a : E), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- dist : E → E → ℝ
- edist : E → E → ENNReal
- edist_dist : ∀ (x y : E), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace E
- uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
- toBornology : Bornology E
The distance function is induced by the norm.
Instances
The distance function is induced by the norm.
Equations
- NormedAddGroup.toSeminormedAddGroup = SeminormedAddGroup.mk ⋯
Equations
- NormedGroup.toSeminormedGroup = SeminormedGroup.mk ⋯
Equations
- NormedAddCommGroup.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯
Equations
- NormedCommGroup.toSeminormedCommGroup = SeminormedCommGroup.mk ⋯
Equations
- SeminormedAddCommGroup.toSeminormedAddGroup = SeminormedAddGroup.mk ⋯
Equations
- SeminormedCommGroup.toSeminormedGroup = SeminormedGroup.mk ⋯
Equations
- NormedAddCommGroup.toNormedAddGroup = NormedAddGroup.mk ⋯
Equations
- NormedCommGroup.toNormedGroup = NormedGroup.mk ⋯
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
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
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
Instances For
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
Instances For
Construct a seminormed group from a translation-invariant pseudodistance.
Equations
Instances For
Construct a seminormed group from a translation-invariant pseudodistance.
Equations
Instances For
Construct a seminormed group from a multiplication-invariant pseudodistance.
Equations
Instances For
Construct a seminormed group from a translation-invariant pseudodistance.
Equations
Instances For
Construct a seminormed group from a multiplication-invariant pseudodistance.
Equations
Instances For
Construct a normed group from a multiplication-invariant distance.
Equations
- NormedGroup.ofMulDist h₁ h₂ = NormedGroup.mk ⋯
Instances For
Construct a normed group from a multiplication-invariant pseudodistance.
Equations
- NormedGroup.ofMulDist' h₁ h₂ = NormedGroup.mk ⋯
Instances For
Construct a normed group from a translation-invariant pseudodistance.
Equations
Instances For
Construct a normed group from a translation-invariant pseudodistance.
Equations
Instances For
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.toSeminormedAddGroup = SeminormedAddGroup.mk ⋯
Instances For
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 = SeminormedGroup.mk ⋯
Instances For
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.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯
Instances For
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 = SeminormedCommGroup.mk ⋯
Instances For
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.toNormedAddGroup = NormedAddGroup.mk ⋯
Instances For
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 = NormedGroup.mk ⋯
Instances For
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.toNormedAddCommGroup = NormedAddCommGroup.mk ⋯
Instances For
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 = NormedCommGroup.mk ⋯
Instances For
Alias of dist_eq_norm_sub
.
Alias of dist_eq_norm_sub'
.
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
Alias of norm_le_norm_add_norm_sub'
.
Alias of norm_le_norm_add_norm_sub
.
The norm of a seminormed group as an additive group seminorm.
Equations
- normAddGroupSeminorm E = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }
Instances For
The norm of a seminormed group as a group seminorm.
Equations
- normGroupSeminorm E = { toFun := norm, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }
Instances For
Alias of nndist_eq_nnnorm_sub
.
Alias of nnnorm_le_nnnorm_add_nnnorm_sub'
.
Alias of nnnorm_le_nnnorm_add_nnnorm_sub
.
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.
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.
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
.
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
.
See tendsto_norm_zero
for a version with pointed neighborhoods.
See tendsto_norm_one
for a version with pointed neighborhoods.
If ‖y‖→∞
, then we can assume y≠x
for any
fixed x
If ‖y‖ → ∞
, then we can assume y ≠ x
for any fixed x
.
A group homomorphism from an AddGroup
to a
SeminormedAddGroup
induces a SeminormedAddGroup
structure on the domain.
Equations
Instances For
A group homomorphism from a Group
to a SeminormedGroup
induces a SeminormedGroup
structure on the domain.
Equations
Instances For
A group homomorphism from an AddCommGroup
to a
SeminormedAddGroup
induces a SeminormedAddCommGroup
structure on the domain.
Equations
Instances For
A group homomorphism from a CommGroup
to a SeminormedGroup
induces a
SeminormedCommGroup
structure on the domain.
Equations
Instances For
An injective group homomorphism from an AddGroup
to a
NormedAddGroup
induces a NormedAddGroup
structure on the domain.
Equations
- NormedAddGroup.induced E F f h = NormedAddGroup.mk ⋯
Instances For
An injective group homomorphism from a Group
to a NormedGroup
induces a NormedGroup
structure on the domain.
Equations
- NormedGroup.induced E F f h = NormedGroup.mk ⋯
Instances For
An injective group homomorphism from a CommGroup
to a
NormedCommGroup
induces a NormedCommGroup
structure on the domain.
Equations
- NormedAddCommGroup.induced E F f h = NormedAddCommGroup.mk ⋯
Instances For
An injective group homomorphism from a CommGroup
to a NormedGroup
induces a
NormedCommGroup
structure on the domain.
Equations
- NormedCommGroup.induced E F f h = NormedCommGroup.mk ⋯
Instances For
Alias of Real.norm_natCast
.
Alias of Real.nnnorm_natCast
.
Equations
- NNReal.instNNNorm = { nnnorm := fun (x : NNReal) => x }
Alias of the forward direction of norm_div_eq_zero_iff
.
See tendsto_norm_zero
for a version with full neighborhoods.
See tendsto_norm_one
for a version with full neighborhoods.
The norm of a normed group as an additive group norm.
Equations
- normAddGroupNorm E = { toAddGroupSeminorm := normAddGroupSeminorm E, eq_zero_of_map_eq_zero' := ⋯ }
Instances For
The norm of a normed group as a group norm.
Equations
- normGroupNorm E = { toGroupSeminorm := normGroupSeminorm E, eq_one_of_map_eq_zero' := ⋯ }
Instances For
Some relations with HasCompactSupport
Alias of the reverse direction of hasCompactSupport_norm_iff
.
Subgroups of normed groups #
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
- AddSubgroup.seminormedAddGroup = SeminormedAddGroup.induced (↥s) E s.subtype
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
- Subgroup.seminormedGroup = SeminormedGroup.induced (↥s) E s.subtype
If x
is an element of a subgroup s
of a seminormed group E
, its
norm in s
is equal to its norm in E
.
If x
is an element of a subgroup s
of a seminormed group E
, its norm in s
is equal to
its norm in E
.
If x
is an element of a subgroup s
of a seminormed group E
,
its norm in s
is equal to its norm in E
.
This is a reversed version of the simp
lemma AddSubgroup.coe_norm
for use by norm_cast
.
If x
is an element of a subgroup s
of a seminormed group E
, its norm in s
is equal to
its norm in E
.
This is a reversed version of the simp
lemma Subgroup.coe_norm
for use by norm_cast
.
Equations
- AddSubgroup.seminormedAddCommGroup = SeminormedAddCommGroup.induced (↥s) E s.subtype
Equations
- Subgroup.seminormedCommGroup = SeminormedCommGroup.induced (↥s) E s.subtype
Equations
- AddSubgroup.normedAddGroup = NormedAddGroup.induced (↥s) E s.subtype ⋯
Equations
- Subgroup.normedGroup = NormedGroup.induced (↥s) E s.subtype ⋯
Equations
- AddSubgroup.normedAddCommGroup = NormedAddCommGroup.induced (↥s) E s.subtype ⋯
Equations
- Subgroup.normedCommGroup = NormedCommGroup.induced (↥s) E s.subtype ⋯
Subgroup classes of normed groups #
A subgroup of a seminormed additive group is also a seminormed additive group, with the restriction of the norm.
Equations
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
- SubgroupClass.seminormedGroup s = SeminormedGroup.induced (↥s) E ↑s
If x
is an element of an additive subgroup s
of a seminormed
additive group E
, its norm in s
is equal to its norm in E
.
If x
is an element of a subgroup s
of a seminormed group E
, its norm in s
is equal to
its norm in E
.
Equations
Equations
Equations
- AddSubgroupClass.normedAddGroup s = NormedAddGroup.induced (↥s) E ↑s ⋯
Equations
- SubgroupClass.normedGroup s = NormedGroup.induced (↥s) E ↑s ⋯
Equations
- AddSubgroupClass.normedAddCommGroup s = NormedAddCommGroup.induced (↥s) E ↑s ⋯
Equations
- SubgroupClass.normedCommGroup s = NormedCommGroup.induced (↥s) E ↑s ⋯