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

@[implicit_reducible]

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 = { norm := fun (a : ↥s) => ‖s.subtype a‖, toGroup := s.toGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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 = { norm := fun (a : ↥s) => ‖s.subtype a‖, toAddGroup := s.toAddGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[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.

@[implicit_reducible]

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

Equations

• Subgroup.seminormedCommGroup = { toNorm := Subgroup.seminormedGroup.toNorm, toCommGroup := s.toCommGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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

Equations

• AddSubgroup.seminormedAddCommGroup = { toNorm := AddSubgroup.seminormedAddGroup.toNorm, toAddCommGroup := s.toAddCommGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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

Equations

• Subgroup.normedGroup = { toNorm := Subgroup.seminormedGroup.toNorm, toGroup := s.toGroup, toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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

Equations

• AddSubgroup.normedAddGroup = { toNorm := AddSubgroup.seminormedAddGroup.toNorm, toAddGroup := s.toAddGroup, toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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

Equations

• Subgroup.normedCommGroup = { toNorm := Subgroup.seminormedCommGroup.toNorm, toCommGroup := s.toCommGroup, toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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

Equations

• AddSubgroup.normedAddCommGroup = { toNorm := AddSubgroup.seminormedAddCommGroup.toNorm, toAddCommGroup := s.toAddCommGroup, toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }

Subgroup classes of normed groups

@[implicit_reducible, 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 = { norm := fun (a : ↥s) => ‖↑s a‖, toGroup := SubgroupClass.toGroup s, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[implicit_reducible, 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 = { norm := fun (a : ↥s) => ‖↑s a‖, toAddGroup := AddSubgroupClass.toAddGroup s, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[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.

@[implicit_reducible, 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

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

@[implicit_reducible, 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

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

@[implicit_reducible, 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 = { toNorm := (SubgroupClass.seminormedGroup s).toNorm, toGroup := (SubgroupClass.seminormedGroup s).toGroup, toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }

@[implicit_reducible, 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

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

@[implicit_reducible, 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

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

@[implicit_reducible, 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

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