Mathlib.Analysis.Normed.Group.Subgroup

Subgroup.seminormedGroup instance

: SeminormedGroup s

Full source

/-- A subgroup of a seminormed group is also a seminormed group,
with the restriction of the norm. -/
@[to_additive "A subgroup of a seminormed group is also a seminormed group, with the restriction of
the norm."]
instance seminormedGroup : SeminormedGroup s :=
  SeminormedGroup.induced _ _ s.subtype

Subgroups Inherit Seminormed Group Structure

Informal description

For any subgroup $s$ of a seminormed group $E$, the subgroup $s$ inherits a seminormed group structure where the norm of an element $x \in s$ is equal to the norm of $x$ considered as an element of $E$.

Subgroup.coe_norm theorem

(x : s) : ‖x‖ = ‖(x : E)‖

Full source

/-- 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`. -/
@[to_additive (attr := simp) "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`."]
theorem coe_norm (x : s) : ‖x‖ = ‖(x : E)‖ :=
  rfl

Norm Equality in Subgroup and Ambient Group: $\|x\|_s = \|x\|_E$

Informal description

For any element $x$ of a subgroup $s$ of a seminormed group $E$, the norm of $x$ in $s$ is equal to the norm of $x$ considered as an element of $E$, i.e., $\|x\|_s = \|x\|_E$.

Subgroup.norm_coe theorem

{s : Subgroup E} (x : s) : ‖(x : E)‖ = ‖x‖

Full source

/-- 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`. -/
@[to_additive (attr := 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 `AddSubgroup.coe_norm` for use by `norm_cast`."]
theorem norm_coe {s : Subgroup E} (x : s) : ‖(x : E)‖ = ‖x‖ :=
  rfl

Equality of Norms in Subgroup and Ambient Group: $\|x_E\| = \|x_s\|$

Informal description

For any subgroup $s$ of a seminormed group $E$ and any element $x \in s$, the norm of $x$ considered as an element of $E$ is equal to the norm of $x$ in the subgroup $s$, i.e., $\|x_E\| = \|x_s\|$.

Subgroup.seminormedCommGroup instance

[SeminormedCommGroup E] {s : Subgroup E} : SeminormedCommGroup s

Full source

@[to_additive]
instance seminormedCommGroup [SeminormedCommGroup E] {s : Subgroup E} : SeminormedCommGroup s :=
  SeminormedCommGroup.induced _ _ s.subtype

Subgroups of Seminormed Commutative Groups are Seminormed Commutative Groups

Informal description

For any seminormed commutative group $E$ and any subgroup $s$ of $E$, the subgroup $s$ inherits a seminormed commutative group structure from $E$.

Subgroup.normedGroup instance

[NormedGroup E] {s : Subgroup E} : NormedGroup s

Full source

@[to_additive]
instance normedGroup [NormedGroup E] {s : Subgroup E} : NormedGroup s :=
  NormedGroup.induced _ _ s.subtype Subtype.coe_injective

Subgroups Inherit Normed Group Structure

Informal description

For any normed group $E$ and any subgroup $s$ of $E$, the subgroup $s$ inherits a normed group structure from $E$.

Subgroup.normedCommGroup instance

[NormedCommGroup E] {s : Subgroup E} : NormedCommGroup s

Full source

@[to_additive]
instance normedCommGroup [NormedCommGroup E] {s : Subgroup E} : NormedCommGroup s :=
  NormedCommGroup.induced _ _ s.subtype Subtype.coe_injective

Subgroups Inherit Normed Commutative Group Structure

Informal description

For any normed commutative group $E$ and any subgroup $s$ of $E$, the subgroup $s$ inherits a normed commutative group structure from $E$.

SubgroupClass.seminormedGroup instance

: SeminormedGroup s

Full source

/-- A subgroup of a seminormed group is also a seminormed group,
with the restriction of the norm. -/
@[to_additive "A subgroup of a seminormed additive group is also a seminormed additive group, with
the restriction of the norm."]
instance (priority := 75) seminormedGroup : SeminormedGroup s :=
  SeminormedGroup.induced _ _ (SubgroupClass.subtype s)

Subgroups Inherit Seminormed Group Structure

Informal description

For any seminormed group $E$ and any subgroup $s$ of $E$ (represented by a set-like structure with subgroup properties), the subgroup $s$ inherits a seminormed group structure where the norm of an element $x \in s$ is equal to its norm in $E$.

SubgroupClass.coe_norm theorem

(x : s) : ‖x‖ = ‖(x : E)‖

Full source

/-- 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`. -/
@[to_additive (attr := simp) "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`."]
theorem coe_norm (x : s) : ‖x‖ = ‖(x : E)‖ :=
  rfl

Norm Equality in Subgroups: $\|x\|_s = \|x\|_E$

Informal description

For any element $x$ in a subgroup $s$ of a seminormed group $E$, the norm of $x$ in $s$ is equal to the norm of $x$ in $E$, i.e., $\|x\|_s = \|x\|_E$.

SubgroupClass.seminormedCommGroup instance

[SeminormedCommGroup E] {S : Type*} [SetLike S E] [SubgroupClass S E] (s : S) : SeminormedCommGroup s

Full source

@[to_additive]
instance (priority := 75) seminormedCommGroup [SeminormedCommGroup E] {S : Type*} [SetLike S E]
    [SubgroupClass S E] (s : S) : SeminormedCommGroup s :=
  SeminormedCommGroup.induced _ _ (SubgroupClass.subtype s)

Subgroups Inherit Seminormed Commutative Group Structure

Informal description

For any seminormed commutative group $E$ and any subgroup $s$ of $E$ (represented by a set-like structure with subgroup properties), the subgroup $s$ inherits a seminormed commutative group structure where the norm of an element $x \in s$ is equal to its norm in $E$.

SubgroupClass.normedGroup instance

[NormedGroup E] {S : Type*} [SetLike S E] [SubgroupClass S E] (s : S) : NormedGroup s

Full source

@[to_additive]
instance (priority := 75) normedGroup [NormedGroup E] {S : Type*} [SetLike S E] [SubgroupClass S E]
    (s : S) : NormedGroup s :=
  NormedGroup.induced _ _ (SubgroupClass.subtype s) Subtype.coe_injective

Subgroups Inherit Normed Group Structure

Informal description

For any normed group $E$ and any subgroup $s$ of $E$ (represented by a set-like structure with subgroup properties), the subgroup $s$ inherits a normed group structure where the norm of an element $x \in s$ is equal to its norm in $E$.

SubgroupClass.normedCommGroup instance

[NormedCommGroup E] {S : Type*} [SetLike S E] [SubgroupClass S E] (s : S) : NormedCommGroup s

Full source

@[to_additive]
instance (priority := 75) normedCommGroup [NormedCommGroup E] {S : Type*} [SetLike S E]
    [SubgroupClass S E] (s : S) : NormedCommGroup s :=
  NormedCommGroup.induced _ _ (SubgroupClass.subtype s) Subtype.coe_injective

Subgroups Inherit Normed Commutative Group Structure

Informal description

For any normed commutative group $E$ and any subgroup $s$ of $E$ (represented by a set-like structure with subgroup properties), the subgroup $s$ inherits a normed commutative group structure where the norm of an element $x \in s$ is equal to its norm in $E$.

Tags