Documentation

Mathlib.Analysis.Normed.Group.Subgroup

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 #

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

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

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

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

      source
      instance Subgroup.seminormedCommGroup {E : Type u_1} [SeminormedCommGroup E] {s : Subgroup E} :
      SeminormedCommGroup ↥s
      Equations
        source
        instance AddSubgroup.seminormedAddCommGroup {E : Type u_1} [SeminormedAddCommGroup E] {s : AddSubgroup E} :
        SeminormedAddCommGroup ↥s
        Equations
          source
          instance Subgroup.normedGroup {E : Type u_1} [NormedGroup E] {s : Subgroup E} :
          NormedGroup ↥s
          Equations
            source
            instance AddSubgroup.normedAddGroup {E : Type u_1} [NormedAddGroup E] {s : AddSubgroup E} :
            NormedAddGroup ↥s
            Equations
              source
              instance Subgroup.normedCommGroup {E : Type u_1} [NormedCommGroup E] {s : Subgroup E} :
              NormedCommGroup ↥s
              Equations
                source
                instance AddSubgroup.normedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] {s : AddSubgroup E} :
                NormedAddCommGroup ↥s
                Equations

                  Subgroup classes of normed groups #

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

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

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