Subgroups of normed (semi)groups

In this file, we prove that subgroups of a normed (semi)group are also normed (semi)groups.

Tags

normed group

Subgroups of normed groups

instance Subgroup.seminormedGroup {E : Type u_1} [SeminormedGroup E] {s : Subgroup E} : SeminormedGroup ↥s

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

instance AddSubgroup.seminormedAddGroup {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} : SeminormedAddGroup ↥s

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

@[simp]

theorem Subgroup.coe_norm {E : Type u_1} [SeminormedGroup E] {s : Subgroup E} (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

@[simp]

theorem AddSubgroup.coe_norm {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s) : ‖x‖ = ‖↑x‖

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 Subgroup.norm_coe {E : Type u_1} [SeminormedGroup E] {s : Subgroup E} (x : ↥s) : ‖↑x‖ = ‖x‖

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.

theorem AddSubgroup.norm_coe {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s) : ‖↑x‖ = ‖x‖

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.

instance Subgroup.seminormedCommGroup {E : Type u_1} [SeminormedCommGroup E] {s : Subgroup E} : SeminormedCommGroup ↥s

Equations

• Subgroup.seminormedCommGroup = SeminormedCommGroup.induced (↥s) E s.subtype

instance AddSubgroup.seminormedAddCommGroup {E : Type u_1} [SeminormedAddCommGroup E] {s : AddSubgroup E} : SeminormedAddCommGroup ↥s

Equations

• AddSubgroup.seminormedAddCommGroup = SeminormedAddCommGroup.induced (↥s) E s.subtype

instance Subgroup.normedGroup {E : Type u_1} [NormedGroup E] {s : Subgroup E} : NormedGroup ↥s

Equations

• Subgroup.normedGroup = NormedGroup.induced (↥s) E s.subtype ⋯

instance AddSubgroup.normedAddGroup {E : Type u_1} [NormedAddGroup E] {s : AddSubgroup E} : NormedAddGroup ↥s

Equations

• AddSubgroup.normedAddGroup = NormedAddGroup.induced (↥s) E s.subtype ⋯

instance Subgroup.normedCommGroup {E : Type u_1} [NormedCommGroup E] {s : Subgroup E} : NormedCommGroup ↥s

Equations

• Subgroup.normedCommGroup = NormedCommGroup.induced (↥s) E s.subtype ⋯

instance AddSubgroup.normedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] {s : AddSubgroup E} : NormedAddCommGroup ↥s

Equations

• AddSubgroup.normedAddCommGroup = NormedAddCommGroup.induced (↥s) E s.subtype ⋯

Subgroup classes of normed groups

@[instance 75]

instance SubgroupClass.seminormedGroup {E : Type u_1} [SeminormedGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) : SeminormedGroup ↥s

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

@[instance 75]

instance AddSubgroupClass.seminormedAddGroup {E : Type u_1} [SeminormedAddGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) : SeminormedAddGroup ↥s

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

Equations

• AddSubgroupClass.seminormedAddGroup s = SeminormedAddGroup.induced (↥s) E ↑s

@[simp]

theorem SubgroupClass.coe_norm {E : Type u_1} [SeminormedGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

@[simp]

theorem AddSubgroupClass.coe_norm {E : Type u_1} [SeminormedAddGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) (x : ↥s) : ‖x‖ = ‖↑x‖

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.

@[instance 75]

instance SubgroupClass.seminormedCommGroup {E : Type u_1} [SeminormedCommGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) : SeminormedCommGroup ↥s

Equations

• SubgroupClass.seminormedCommGroup s = SeminormedCommGroup.induced (↥s) E ↑s

@[instance 75]

instance AddSubgroupClass.seminormedAddCommGroup {E : Type u_1} [SeminormedAddCommGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) : SeminormedAddCommGroup ↥s

Equations

• AddSubgroupClass.seminormedAddCommGroup s = SeminormedAddCommGroup.induced (↥s) E ↑s

@[instance 75]

instance SubgroupClass.normedGroup {E : Type u_1} [NormedGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) : NormedGroup ↥s

Equations

• SubgroupClass.normedGroup s = NormedGroup.induced (↥s) E ↑s ⋯

@[instance 75]

instance AddSubgroupClass.normedAddGroup {E : Type u_1} [NormedAddGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) : NormedAddGroup ↥s

Equations

• AddSubgroupClass.normedAddGroup s = NormedAddGroup.induced (↥s) E ↑s ⋯

@[instance 75]

instance SubgroupClass.normedCommGroup {E : Type u_1} [NormedCommGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) : NormedCommGroup ↥s

Equations

• SubgroupClass.normedCommGroup s = NormedCommGroup.induced (↥s) E ↑s ⋯

@[instance 75]

instance AddSubgroupClass.normedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) : NormedAddCommGroup ↥s

Equations

• AddSubgroupClass.normedAddCommGroup s = NormedAddCommGroup.induced (↥s) E ↑s ⋯