Documentation

Mathlib.Analysis.Normed.Group.Basic

Normed (semi)groups #

In this file we define 10 classes:

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

class Norm (E : Type u_9) :
Type u_9

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This class is designed to be extended in more interesting classes specifying the properties of the norm.

  • norm : E

    the -valued norm function.

Instances
    class NNNorm (E : Type u_9) :
    Type u_9

    Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ‖x‖₊.

    • nnnorm : ENNReal

      the ℝ≥0-valued norm function.

    Instances

      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
          class SeminormedAddGroup (E : Type u_9) extends Norm , AddGroup , PseudoMetricSpace :
          Type u_9

          A seminormed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a pseudometric space structure.

          Instances
            class SeminormedGroup (E : Type u_9) extends Norm , Group , PseudoMetricSpace :
            Type u_9

            A seminormed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a pseudometric space structure.

            Instances
              class NormedAddGroup (E : Type u_9) extends Norm , AddGroup , MetricSpace :
              Type u_9

              A normed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a metric space structure.

              Instances
                class NormedGroup (E : Type u_9) extends Norm , Group , MetricSpace :
                Type u_9

                A normed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a metric space structure.

                Instances

                  A seminormed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a pseudometric space structure.

                  Instances
                    class SeminormedCommGroup (E : Type u_9) extends Norm , CommGroup , PseudoMetricSpace :
                    Type u_9

                    A seminormed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a pseudometric space structure.

                    Instances
                      class NormedAddCommGroup (E : Type u_9) extends Norm , AddCommGroup , MetricSpace :
                      Type u_9

                      A normed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a metric space structure.

                      Instances
                        class NormedCommGroup (E : Type u_9) extends Norm , CommGroup , MetricSpace :
                        Type u_9

                        A normed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a metric space structure.

                        Instances
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          @[reducible]
                          def NormedAddGroup.ofSeparation {E : Type u_6} [SeminormedAddGroup E] (h : ∀ (x : E), x = 0x = 0) :

                          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
                            theorem NormedAddGroup.ofSeparation.proof_1 {E : Type u_1} [SeminormedAddGroup E] (h : ∀ (x : E), x = 0x = 0) :
                            ∀ {x y : E}, dist x y = 0x = y
                            @[reducible]
                            def NormedGroup.ofSeparation {E : Type u_6} [SeminormedGroup E] (h : ∀ (x : E), x = 0x = 1) :

                            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
                              theorem NormedAddCommGroup.ofSeparation.proof_1 {E : Type u_1} [SeminormedAddCommGroup E] (h : ∀ (x : E), x = 0x = 0) :
                              ∀ {x y : E}, dist x y = 0x = y
                              @[reducible]
                              def NormedAddCommGroup.ofSeparation {E : Type u_6} [SeminormedAddCommGroup E] (h : ∀ (x : E), x = 0x = 0) :

                              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
                                @[reducible]
                                def NormedCommGroup.ofSeparation {E : Type u_6} [SeminormedCommGroup E] (h : ∀ (x : E), x = 0x = 1) :

                                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
                                  theorem SeminormedAddGroup.ofAddDist.proof_1 {E : Type u_1} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) (x : E) (y : E) :
                                  dist x y = x - y
                                  @[reducible]
                                  def SeminormedAddGroup.ofAddDist {E : Type u_6} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

                                  Construct a seminormed group from a translation-invariant distance.

                                  Equations
                                  Instances For
                                    @[reducible]
                                    def SeminormedGroup.ofMulDist {E : Type u_6} [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

                                    Construct a seminormed group from a multiplication-invariant distance.

                                    Equations
                                    Instances For
                                      @[reducible]
                                      def SeminormedAddGroup.ofAddDist' {E : Type u_6} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

                                      Construct a seminormed group from a translation-invariant pseudodistance.

                                      Equations
                                      Instances For
                                        theorem SeminormedAddGroup.ofAddDist'.proof_1 {E : Type u_1} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) (x : E) (y : E) :
                                        dist x y = x - y
                                        @[reducible]
                                        def SeminormedGroup.ofMulDist' {E : Type u_6} [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

                                        Construct a seminormed group from a multiplication-invariant pseudodistance.

                                        Equations
                                        Instances For
                                          @[reducible]
                                          def SeminormedAddCommGroup.ofAddDist {E : Type u_6} [Norm E] [AddCommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

                                          Construct a seminormed group from a translation-invariant pseudodistance.

                                          Equations
                                          Instances For
                                            theorem SeminormedAddCommGroup.ofAddDist.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                            a + b = b + a
                                            @[reducible]
                                            def SeminormedCommGroup.ofMulDist {E : Type u_6} [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

                                            Construct a seminormed group from a multiplication-invariant pseudodistance.

                                            Equations
                                            Instances For
                                              @[reducible]
                                              def SeminormedAddCommGroup.ofAddDist' {E : Type u_6} [Norm E] [AddCommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

                                              Construct a seminormed group from a translation-invariant pseudodistance.

                                              Equations
                                              Instances For
                                                theorem SeminormedAddCommGroup.ofAddDist'.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                a + b = b + a
                                                @[reducible]
                                                def SeminormedCommGroup.ofMulDist' {E : Type u_6} [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

                                                Construct a seminormed group from a multiplication-invariant pseudodistance.

                                                Equations
                                                Instances For
                                                  @[reducible]
                                                  def NormedAddGroup.ofAddDist {E : Type u_6} [Norm E] [AddGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

                                                  Construct a normed group from a translation-invariant distance.

                                                  Equations
                                                  Instances For
                                                    @[reducible]
                                                    def NormedGroup.ofMulDist {E : Type u_6} [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

                                                    Construct a normed group from a multiplication-invariant distance.

                                                    Equations
                                                    Instances For
                                                      @[reducible]
                                                      def NormedAddGroup.ofAddDist' {E : Type u_6} [Norm E] [AddGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

                                                      Construct a normed group from a translation-invariant pseudodistance.

                                                      Equations
                                                      Instances For
                                                        @[reducible]
                                                        def NormedGroup.ofMulDist' {E : Type u_6} [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

                                                        Construct a normed group from a multiplication-invariant pseudodistance.

                                                        Equations
                                                        Instances For
                                                          theorem NormedAddCommGroup.ofAddDist.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                          a + b = b + a
                                                          @[reducible]
                                                          def NormedAddCommGroup.ofAddDist {E : Type u_6} [Norm E] [AddCommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

                                                          Construct a normed group from a translation-invariant pseudodistance.

                                                          Equations
                                                          Instances For
                                                            @[reducible]
                                                            def NormedCommGroup.ofMulDist {E : Type u_6} [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist x y dist (x * z) (y * z)) :

                                                            Construct a normed group from a multiplication-invariant pseudodistance.

                                                            Equations
                                                            Instances For
                                                              @[reducible]
                                                              def NormedAddCommGroup.ofAddDist' {E : Type u_6} [Norm E] [AddCommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

                                                              Construct a normed group from a translation-invariant pseudodistance.

                                                              Equations
                                                              Instances For
                                                                theorem NormedAddCommGroup.ofAddDist'.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                                a + b = b + a
                                                                @[reducible]
                                                                def NormedCommGroup.ofMulDist' {E : Type u_6} [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) dist x y) :

                                                                Construct a normed group from a multiplication-invariant pseudodistance.

                                                                Equations
                                                                Instances For
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) :
                                                                  f (x - x) = 0
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_2 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                  f (x - y) = f (y - x)
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_3 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (a : E) (b : E) (c : E) :
                                                                  f (a - c) f (a - b) + f (b - c)
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_4 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                  0 f (x - y)
                                                                  @[reducible]

                                                                  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
                                                                  Instances For
                                                                    theorem AddGroupSeminorm.toSeminormedAddGroup.proof_8 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                    dist x y = dist x y
                                                                    theorem AddGroupSeminorm.toSeminormedAddGroup.proof_5 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                    { val := f (x - y), property := } = ENNReal.ofReal { val := f (x - y), property := }
                                                                    @[reducible]

                                                                    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
                                                                    Instances For
                                                                      theorem AddGroupSeminorm.toSeminormedAddCommGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                                      a + b = b + a
                                                                      @[reducible]

                                                                      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
                                                                      Instances For
                                                                        @[reducible]

                                                                        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
                                                                        Instances For
                                                                          @[reducible]

                                                                          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
                                                                          Instances For
                                                                            theorem AddGroupNorm.toNormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) :
                                                                            ∀ {x y : E}, dist x y = 0x = y
                                                                            @[reducible]

                                                                            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
                                                                            Instances For
                                                                              @[reducible]

                                                                              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
                                                                              Instances For
                                                                                theorem AddGroupNorm.toNormedAddCommGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                                                a + b = b + a
                                                                                @[reducible]

                                                                                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
                                                                                Instances For
                                                                                  theorem dist_eq_norm_sub {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = a - b
                                                                                  theorem dist_eq_norm_div {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist a b = a / b
                                                                                  theorem dist_eq_norm_sub' {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = b - a
                                                                                  theorem dist_eq_norm_div' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist a b = b / a
                                                                                  theorem dist_eq_norm {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = a - b

                                                                                  Alias of dist_eq_norm_sub.

                                                                                  theorem dist_eq_norm' {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = b - a

                                                                                  Alias of dist_eq_norm_sub'.

                                                                                  @[simp]
                                                                                  theorem dist_zero_right {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem dist_one_right {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem dist_zero_left {E : Type u_6} [SeminormedAddGroup E] :
                                                                                  dist 0 = norm
                                                                                  @[simp]
                                                                                  theorem dist_one_left {E : Type u_6} [SeminormedGroup E] :
                                                                                  dist 1 = norm
                                                                                  theorem Isometry.norm_map_of_map_zero {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :
                                                                                  theorem Isometry.norm_map_of_map_one {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
                                                                                  @[simp]
                                                                                  theorem comap_norm_atTop {E : Type u_6} [SeminormedAddGroup E] :
                                                                                  Filter.comap norm Filter.atTop = Bornology.cobounded E
                                                                                  @[simp]
                                                                                  theorem comap_norm_atTop' {E : Type u_6} [SeminormedGroup E] :
                                                                                  Filter.comap norm Filter.atTop = Bornology.cobounded E
                                                                                  theorem Filter.HasBasis.cobounded_of_norm {E : Type u_6} [SeminormedAddGroup E] {ι : Sort u_9} {p : ιProp} {s : ιSet } (h : Filter.HasBasis Filter.atTop p s) :
                                                                                  Filter.HasBasis (Bornology.cobounded E) p fun (i : ι) => norm ⁻¹' s i
                                                                                  theorem Filter.HasBasis.cobounded_of_norm' {E : Type u_6} [SeminormedGroup E] {ι : Sort u_9} {p : ιProp} {s : ιSet } (h : Filter.HasBasis Filter.atTop p s) :
                                                                                  Filter.HasBasis (Bornology.cobounded E) p fun (i : ι) => norm ⁻¹' s i
                                                                                  theorem Filter.hasBasis_cobounded_norm {E : Type u_6} [SeminormedAddGroup E] :
                                                                                  Filter.HasBasis (Bornology.cobounded E) (fun (x : ) => True) fun (x : ) => {x_1 : E | x x_1}
                                                                                  theorem Filter.hasBasis_cobounded_norm' {E : Type u_6} [SeminormedGroup E] :
                                                                                  Filter.HasBasis (Bornology.cobounded E) (fun (x : ) => True) fun (x : ) => {x_1 : E | x x_1}
                                                                                  @[simp]
                                                                                  theorem tendsto_norm_atTop_iff_cobounded {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : αE} {l : Filter α} :
                                                                                  Filter.Tendsto (fun (x : α) => f x) l Filter.atTop Filter.Tendsto f l (Bornology.cobounded E)
                                                                                  @[simp]
                                                                                  theorem tendsto_norm_atTop_iff_cobounded' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : αE} {l : Filter α} :
                                                                                  Filter.Tendsto (fun (x : α) => f x) l Filter.atTop Filter.Tendsto f l (Bornology.cobounded E)
                                                                                  theorem eventually_cobounded_le_norm {E : Type u_6} [SeminormedAddGroup E] (a : ) :
                                                                                  ∀ᶠ (x : E) in Bornology.cobounded E, a x
                                                                                  theorem eventually_cobounded_le_norm' {E : Type u_6} [SeminormedGroup E] (a : ) :
                                                                                  ∀ᶠ (x : E) in Bornology.cobounded E, a x
                                                                                  theorem norm_sub_rev {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  a - b = b - a
                                                                                  theorem norm_div_rev {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  a / b = b / a
                                                                                  @[simp]
                                                                                  theorem norm_neg {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem norm_inv' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                  theorem dist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                  theorem dist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                  @[simp]
                                                                                  theorem dist_add_self_right {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist b (a + b) = a
                                                                                  @[simp]
                                                                                  theorem dist_mul_self_right {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist b (a * b) = a
                                                                                  @[simp]
                                                                                  theorem dist_add_self_left {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist (a + b) b = a
                                                                                  @[simp]
                                                                                  theorem dist_mul_self_left {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist (a * b) b = a
                                                                                  @[simp]
                                                                                  theorem dist_sub_eq_dist_add_left {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist (a - b) c = dist a (c + b)
                                                                                  @[simp]
                                                                                  theorem dist_div_eq_dist_mul_left {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist (a / b) c = dist a (c * b)
                                                                                  @[simp]
                                                                                  theorem dist_sub_eq_dist_add_right {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist a (b - c) = dist (a + c) b
                                                                                  @[simp]
                                                                                  theorem dist_div_eq_dist_mul_right {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist a (b / c) = dist (a * c) b

                                                                                  In a (semi)normed group, negation x ↦ -x tends to infinity at infinity.

                                                                                  In a (semi)normed group, inversion x ↦ x⁻¹ tends to infinity at infinity.

                                                                                  theorem norm_add_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :

                                                                                  Triangle inequality for the norm.

                                                                                  theorem norm_mul_le' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :

                                                                                  Triangle inequality for the norm.

                                                                                  theorem norm_add_le_of_le {E : Type u_6} [SeminormedAddGroup E] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
                                                                                  a₁ + a₂ r₁ + r₂
                                                                                  theorem norm_mul_le_of_le {E : Type u_6} [SeminormedGroup E] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
                                                                                  a₁ * a₂ r₁ + r₂
                                                                                  theorem norm_add₃_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  theorem norm_mul₃_le {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  theorem norm_sub_le_norm_sub_add_norm_sub {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  theorem norm_div_le_norm_div_add_norm_div {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  @[simp]
                                                                                  theorem norm_nonneg {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem norm_nonneg' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem abs_norm {E : Type u_6} [SeminormedAddGroup E] (z : E) :
                                                                                  @[simp]
                                                                                  theorem abs_norm' {E : Type u_6} [SeminormedGroup E] (z : E) :

                                                                                  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
                                                                                      @[simp]
                                                                                      theorem norm_zero {E : Type u_6} [SeminormedAddGroup E] :
                                                                                      @[simp]
                                                                                      theorem norm_one' {E : Type u_6} [SeminormedGroup E] :
                                                                                      theorem ne_zero_of_norm_ne_zero {E : Type u_6} [SeminormedAddGroup E] {a : E} :
                                                                                      a 0a 0
                                                                                      theorem ne_one_of_norm_ne_zero {E : Type u_6} [SeminormedGroup E] {a : E} :
                                                                                      a 0a 1
                                                                                      theorem zero_lt_one_add_norm_sq {E : Type u_6} [SeminormedAddGroup E] (x : E) :
                                                                                      0 < 1 + x ^ 2
                                                                                      theorem zero_lt_one_add_norm_sq' {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                      0 < 1 + x ^ 2
                                                                                      theorem norm_sub_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                      theorem norm_div_le {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                      theorem norm_sub_le_of_le {E : Type u_6} [SeminormedAddGroup E] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (H₁ : a₁ r₁) (H₂ : a₂ r₂) :
                                                                                      a₁ - a₂ r₁ + r₂
                                                                                      theorem norm_div_le_of_le {E : Type u_6} [SeminormedGroup E] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (H₁ : a₁ r₁) (H₂ : a₂ r₂) :
                                                                                      a₁ / a₂ r₁ + r₂
                                                                                      theorem dist_le_norm_add_norm {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                      theorem dist_le_norm_add_norm' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                      theorem abs_norm_sub_norm_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                      theorem abs_norm_sub_norm_le' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                      theorem norm_sub_norm_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                      theorem norm_sub_norm_le' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                      theorem dist_norm_norm_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                      theorem dist_norm_norm_le' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                      theorem norm_le_norm_add_norm_sub' {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) :
                                                                                      theorem norm_le_norm_add_norm_div' {E : Type u_6} [SeminormedGroup E] (u : E) (v : E) :
                                                                                      theorem norm_le_norm_add_norm_sub {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) :
                                                                                      theorem norm_le_norm_add_norm_div {E : Type u_6} [SeminormedGroup E] (u : E) (v : E) :
                                                                                      theorem norm_le_insert' {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) :

                                                                                      Alias of norm_le_norm_add_norm_sub'.

                                                                                      theorem norm_le_insert {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) :

                                                                                      Alias of norm_le_norm_add_norm_sub.

                                                                                      theorem norm_le_add_norm_add {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) :
                                                                                      theorem norm_le_mul_norm_add {E : Type u_6} [SeminormedGroup E] (u : E) (v : E) :
                                                                                      theorem ball_eq {E : Type u_6} [SeminormedAddGroup E] (y : E) (ε : ) :
                                                                                      Metric.ball y ε = {x : E | x - y < ε}
                                                                                      theorem ball_eq' {E : Type u_6} [SeminormedGroup E] (y : E) (ε : ) :
                                                                                      Metric.ball y ε = {x : E | x / y < ε}
                                                                                      theorem ball_zero_eq {E : Type u_6} [SeminormedAddGroup E] (r : ) :
                                                                                      Metric.ball 0 r = {x : E | x < r}
                                                                                      theorem ball_one_eq {E : Type u_6} [SeminormedGroup E] (r : ) :
                                                                                      Metric.ball 1 r = {x : E | x < r}
                                                                                      theorem mem_ball_iff_norm {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_iff_norm'' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_iff_norm' {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_iff_norm''' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_zero_iff {E : Type u_6} [SeminormedAddGroup E] {a : E} {r : } :
                                                                                      theorem mem_ball_one_iff {E : Type u_6} [SeminormedGroup E] {a : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm'' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm' {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm''' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem norm_le_of_mem_closedBall {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } (h : b Metric.closedBall a r) :
                                                                                      theorem norm_le_of_mem_closedBall' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } (h : b Metric.closedBall a r) :
                                                                                      theorem norm_le_norm_add_const_of_dist_le {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      dist a b ra b + r
                                                                                      theorem norm_le_norm_add_const_of_dist_le' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      dist a b ra b + r
                                                                                      theorem norm_lt_of_mem_ball {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } (h : b Metric.ball a r) :
                                                                                      theorem norm_lt_of_mem_ball' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } (h : b Metric.ball a r) :
                                                                                      theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) (w : E) :
                                                                                      theorem norm_div_sub_norm_div_le_norm_div {E : Type u_6} [SeminormedGroup E] (u : E) (v : E) (w : E) :
                                                                                      theorem isBounded_iff_forall_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded s ∃ (C : ), xs, x C
                                                                                      theorem isBounded_iff_forall_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded s ∃ (C : ), xs, x C
                                                                                      theorem Bornology.IsBounded.exists_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded s∃ (C : ), xs, x C

                                                                                      Alias of the forward direction of isBounded_iff_forall_norm_le'.

                                                                                      theorem Bornology.IsBounded.exists_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded s∃ (C : ), xs, x C

                                                                                      Alias of the forward direction of isBounded_iff_forall_norm_le.

                                                                                      theorem Bornology.IsBounded.exists_pos_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
                                                                                      ∃ R > 0, xs, x R
                                                                                      abbrev Bornology.IsBounded.exists_pos_norm_le.match_1 {E : Type u_1} [SeminormedAddGroup E] {s : Set E} (motive : (∃ (C : ), xs, x C)Prop) :
                                                                                      ∀ (x : ∃ (C : ), xs, x C), (∀ (R₀ : ) (hR₀ : xs, x R₀), motive )motive x
                                                                                      Equations
                                                                                      • =
                                                                                      Instances For
                                                                                        theorem Bornology.IsBounded.exists_pos_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
                                                                                        ∃ R > 0, xs, x R
                                                                                        abbrev Bornology.IsBounded.exists_pos_norm_lt.match_1 {E : Type u_1} [SeminormedAddGroup E] {s : Set E} (motive : (∃ R > 0, xs, x R)Prop) :
                                                                                        ∀ (x : ∃ R > 0, xs, x R), (∀ (R : ) (hR₀ : R > 0) (hR : xs, x R), motive )motive x
                                                                                        Equations
                                                                                        • =
                                                                                        Instances For
                                                                                          theorem Bornology.IsBounded.exists_pos_norm_lt {E : Type u_6} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
                                                                                          ∃ R > 0, xs, x < R
                                                                                          theorem Bornology.IsBounded.exists_pos_norm_lt' {E : Type u_6} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) :
                                                                                          ∃ R > 0, xs, x < R
                                                                                          @[simp]
                                                                                          theorem mem_sphere_iff_norm {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                          @[simp]
                                                                                          theorem mem_sphere_iff_norm' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                          theorem mem_sphere_zero_iff_norm {E : Type u_6} [SeminormedAddGroup E] {a : E} {r : } :
                                                                                          theorem mem_sphere_one_iff_norm {E : Type u_6} [SeminormedGroup E] {a : E} {r : } :
                                                                                          @[simp]
                                                                                          theorem norm_eq_of_mem_sphere {E : Type u_6} [SeminormedAddGroup E] {r : } (x : (Metric.sphere 0 r)) :
                                                                                          x = r
                                                                                          @[simp]
                                                                                          theorem norm_eq_of_mem_sphere' {E : Type u_6} [SeminormedGroup E] {r : } (x : (Metric.sphere 1 r)) :
                                                                                          x = r
                                                                                          theorem ne_zero_of_mem_sphere {E : Type u_6} [SeminormedAddGroup E] {r : } (hr : r 0) (x : (Metric.sphere 0 r)) :
                                                                                          x 0
                                                                                          theorem ne_one_of_mem_sphere {E : Type u_6} [SeminormedGroup E] {r : } (hr : r 0) (x : (Metric.sphere 1 r)) :
                                                                                          x 1
                                                                                          theorem ne_zero_of_mem_unit_sphere {E : Type u_6} [SeminormedAddGroup E] (x : (Metric.sphere 0 1)) :
                                                                                          x 0
                                                                                          theorem ne_one_of_mem_unit_sphere {E : Type u_6} [SeminormedGroup E] (x : (Metric.sphere 1 1)) :
                                                                                          x 1

                                                                                          The norm of a seminormed group as an additive group seminorm.

                                                                                          Equations
                                                                                          Instances For

                                                                                            The norm of a seminormed group as a group seminorm.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem coe_normGroupSeminorm (E : Type u_6) [SeminormedGroup E] :
                                                                                              (normGroupSeminorm E) = norm
                                                                                              theorem NormedAddCommGroup.tendsto_nhds_zero {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : αE} {l : Filter α} :
                                                                                              Filter.Tendsto f l (nhds 0) ε > 0, ∀ᶠ (x : α) in l, f x < ε
                                                                                              theorem NormedCommGroup.tendsto_nhds_one {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : αE} {l : Filter α} :
                                                                                              Filter.Tendsto f l (nhds 1) ε > 0, ∀ᶠ (x : α) in l, f x < ε
                                                                                              theorem NormedAddCommGroup.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {x : E} {y : F} :
                                                                                              Filter.Tendsto f (nhds x) (nhds y) ε > 0, ∃ δ > 0, ∀ (x' : E), x' - x < δf x' - y < ε
                                                                                              theorem NormedCommGroup.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {x : E} {y : F} :
                                                                                              Filter.Tendsto f (nhds x) (nhds y) ε > 0, ∃ δ > 0, ∀ (x' : E), x' / x < δf x' / y < ε
                                                                                              theorem NormedAddCommGroup.cauchySeq_iff {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [Nonempty α] [SemilatticeSup α] {u : αE} :
                                                                                              CauchySeq u ε > 0, ∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m - u n < ε
                                                                                              theorem NormedCommGroup.cauchySeq_iff {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [Nonempty α] [SemilatticeSup α] {u : αE} :
                                                                                              CauchySeq u ε > 0, ∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m / u n < ε
                                                                                              theorem NormedAddCommGroup.nhds_basis_norm_lt {E : Type u_6} [SeminormedAddGroup E] (x : E) :
                                                                                              Filter.HasBasis (nhds x) (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y - x < ε}
                                                                                              theorem NormedCommGroup.nhds_basis_norm_lt {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                              Filter.HasBasis (nhds x) (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y / x < ε}
                                                                                              theorem NormedAddCommGroup.nhds_zero_basis_norm_lt {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              Filter.HasBasis (nhds 0) (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y < ε}
                                                                                              theorem NormedCommGroup.nhds_one_basis_norm_lt {E : Type u_6} [SeminormedGroup E] :
                                                                                              Filter.HasBasis (nhds 1) (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y < ε}
                                                                                              theorem NormedAddCommGroup.uniformity_basis_dist {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              Filter.HasBasis (uniformity E) (fun (ε : ) => 0 < ε) fun (ε : ) => {p : E × E | p.1 - p.2 < ε}
                                                                                              theorem NormedCommGroup.uniformity_basis_dist {E : Type u_6} [SeminormedGroup E] :
                                                                                              Filter.HasBasis (uniformity E) (fun (ε : ) => 0 < ε) fun (ε : ) => {p : E × E | p.1 / p.2 < ε}
                                                                                              theorem AddMonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :

                                                                                              A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/NormedSpace/OperatorNorm.lean.

                                                                                              theorem MonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :

                                                                                              A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/NormedSpace/OperatorNorm.lean.

                                                                                              theorem lipschitzOnWith_iff_norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : EF} {C : NNReal} :
                                                                                              LipschitzOnWith C f s ∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x - f y C * x - y
                                                                                              theorem lipschitzOnWith_iff_norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : EF} {C : NNReal} :
                                                                                              LipschitzOnWith C f s ∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x / f y C * x / y
                                                                                              theorem LipschitzOnWith.norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : EF} {C : NNReal} :
                                                                                              LipschitzOnWith C f s∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x / f y C * x / y

                                                                                              Alias of the forward direction of lipschitzOnWith_iff_norm_div_le.

                                                                                              theorem LipschitzOnWith.norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : EF} {C : NNReal} :
                                                                                              LipschitzOnWith C f s∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x - f y C * x - y
                                                                                              theorem LipschitzOnWith.norm_sub_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a s) (hb : b s) (hr : a - b r) :
                                                                                              f a - f b C * r
                                                                                              theorem LipschitzOnWith.norm_div_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a s) (hb : b s) (hr : a / b r) :
                                                                                              f a / f b C * r
                                                                                              theorem lipschitzWith_iff_norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {C : NNReal} :
                                                                                              LipschitzWith C f ∀ (x y : E), f x - f y C * x - y
                                                                                              theorem lipschitzWith_iff_norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {C : NNReal} :
                                                                                              LipschitzWith C f ∀ (x y : E), f x / f y C * x / y
                                                                                              theorem LipschitzWith.norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {C : NNReal} :
                                                                                              LipschitzWith C f∀ (x y : E), f x / f y C * x / y

                                                                                              Alias of the forward direction of lipschitzWith_iff_norm_div_le.

                                                                                              theorem LipschitzWith.norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {C : NNReal} :
                                                                                              LipschitzWith C f∀ (x y : E), f x - f y C * x - y
                                                                                              theorem LipschitzWith.norm_sub_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzWith C f) (hr : a - b r) :
                                                                                              f a - f b C * r
                                                                                              theorem LipschitzWith.norm_div_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzWith C f) (hr : a / b r) :
                                                                                              f a / f b C * r
                                                                                              theorem AddMonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :

                                                                                              A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖

                                                                                              theorem MonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :

                                                                                              A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖.

                                                                                              theorem AddMonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :
                                                                                              theorem MonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :
                                                                                              theorem IsCompact.exists_bound_of_continuousOn {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : αE} (hf : ContinuousOn f s) :
                                                                                              ∃ (C : ), xs, f x C
                                                                                              theorem IsCompact.exists_bound_of_continuousOn' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : αE} (hf : ContinuousOn f s) :
                                                                                              ∃ (C : ), xs, f x C
                                                                                              theorem HasCompactSupport.exists_bound_of_continuous {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} (hf : HasCompactSupport f) (h'f : Continuous f) :
                                                                                              ∃ (C : ), ∀ (x : α), f x C
                                                                                              theorem HasCompactMulSupport.exists_bound_of_continuous {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} (hf : HasCompactMulSupport f) (h'f : Continuous f) :
                                                                                              ∃ (C : ), ∀ (x : α), f x C
                                                                                              theorem AddMonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) :
                                                                                              Isometry f ∀ (x : E), f x = x
                                                                                              theorem MonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) :
                                                                                              Isometry f ∀ (x : E), f x = x
                                                                                              theorem MonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) :
                                                                                              (∀ (x : E), f x = x)Isometry f

                                                                                              Alias of the reverse direction of MonoidHomClass.isometry_iff_norm.

                                                                                              theorem AddMonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) :
                                                                                              (∀ (x : E), f x = x)Isometry f
                                                                                              Equations
                                                                                              • SeminormedAddGroup.toNNNorm = { nnnorm := fun (a : E) => { val := a, property := } }
                                                                                              Equations
                                                                                              • SeminormedGroup.toNNNorm = { nnnorm := fun (a : E) => { val := a, property := } }
                                                                                              @[simp]
                                                                                              theorem coe_nnnorm {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                              @[simp]
                                                                                              theorem coe_nnnorm' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                              @[simp]
                                                                                              theorem coe_comp_nnnorm {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              NNReal.toReal nnnorm = norm
                                                                                              @[simp]
                                                                                              theorem coe_comp_nnnorm' {E : Type u_6} [SeminormedGroup E] :
                                                                                              NNReal.toReal nnnorm = norm
                                                                                              theorem nndist_eq_nnnorm_sub {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                              theorem nndist_eq_nnnorm_div {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                              theorem nndist_eq_nnnorm {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :

                                                                                              Alias of nndist_eq_nnnorm_sub.

                                                                                              @[simp]
                                                                                              theorem nnnorm_zero {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              @[simp]
                                                                                              theorem nnnorm_one' {E : Type u_6} [SeminormedGroup E] :
                                                                                              theorem ne_zero_of_nnnorm_ne_zero {E : Type u_6} [SeminormedAddGroup E] {a : E} :
                                                                                              a‖₊ 0a 0
                                                                                              theorem ne_one_of_nnnorm_ne_zero {E : Type u_6} [SeminormedGroup E] {a : E} :
                                                                                              a‖₊ 0a 1
                                                                                              theorem nnnorm_add_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                              theorem nnnorm_mul_le' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                              @[simp]
                                                                                              theorem nnnorm_neg {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                              @[simp]
                                                                                              theorem nnnorm_inv' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                              theorem nndist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                              theorem nndist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                              theorem nnnorm_sub_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                              theorem nnnorm_div_le {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                              theorem edist_eq_coe_nnnorm_sub {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                              edist a b = a - b‖₊
                                                                                              theorem edist_eq_coe_nnnorm_div {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                              edist a b = a / b‖₊
                                                                                              theorem edist_eq_coe_nnnorm {E : Type u_6} [SeminormedAddGroup E] (x : E) :
                                                                                              edist x 0 = x‖₊
                                                                                              theorem edist_eq_coe_nnnorm' {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                              edist x 1 = x‖₊
                                                                                              theorem edist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                              theorem edist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                              theorem mem_emetric_ball_one_iff {E : Type u_6} [SeminormedGroup E] {a : E} {r : ENNReal} :
                                                                                              theorem AddMonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), f x‖₊ C * x‖₊) :
                                                                                              theorem MonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), f x‖₊ C * x‖₊) :
                                                                                              theorem AddMonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), x K * f x) :
                                                                                              theorem MonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), x K * f x) :
                                                                                              theorem LipschitzWith.norm_le_mul {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                              f x K * x
                                                                                              theorem LipschitzWith.norm_le_mul' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                              f x K * x
                                                                                              theorem LipschitzWith.nnorm_le_mul {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                              theorem LipschitzWith.nnorm_le_mul' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                              theorem AntilipschitzWith.le_mul_norm {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                              x K * f x
                                                                                              theorem AntilipschitzWith.le_mul_norm' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                              x K * f x
                                                                                              theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                              theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                              theorem ZeroHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
                                                                                              x K * f x
                                                                                              theorem OneHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
                                                                                              x K * f x
                                                                                              theorem Isometry.nnnorm_map_of_map_zero {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :
                                                                                              theorem Isometry.nnnorm_map_of_map_one {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
                                                                                              theorem tendsto_iff_norm_sub_tendsto_zero {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : αE} {a : Filter α} {b : E} :
                                                                                              Filter.Tendsto f a (nhds b) Filter.Tendsto (fun (e : α) => f e - b) a (nhds 0)
                                                                                              theorem tendsto_iff_norm_div_tendsto_zero {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : αE} {a : Filter α} {b : E} :
                                                                                              Filter.Tendsto f a (nhds b) Filter.Tendsto (fun (e : α) => f e / b) a (nhds 0)
                                                                                              theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : αE} {a : Filter α} :
                                                                                              Filter.Tendsto f a (nhds 0) Filter.Tendsto (fun (x : α) => f x) a (nhds 0)
                                                                                              theorem tendsto_one_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : αE} {a : Filter α} :
                                                                                              Filter.Tendsto f a (nhds 1) Filter.Tendsto (fun (x : α) => f x) a (nhds 0)
                                                                                              theorem squeeze_zero_norm' {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : αE} {a : α} {t₀ : Filter α} (h : ∀ᶠ (n : α) in t₀, f n a n) (h' : Filter.Tendsto a t₀ (nhds 0)) :
                                                                                              Filter.Tendsto f t₀ (nhds 0)

                                                                                              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.PseudoMetric and Topology.Algebra.Order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

                                                                                              theorem squeeze_one_norm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : αE} {a : α} {t₀ : Filter α} (h : ∀ᶠ (n : α) in t₀, f n a n) (h' : Filter.Tendsto a t₀ (nhds 0)) :
                                                                                              Filter.Tendsto f t₀ (nhds 1)

                                                                                              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.

                                                                                              theorem squeeze_zero_norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : αE} {a : α} {t₀ : Filter α} (h : ∀ (n : α), f n a n) :
                                                                                              Filter.Tendsto a t₀ (nhds 0)Filter.Tendsto f t₀ (nhds 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 0.

                                                                                              theorem squeeze_one_norm {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : αE} {a : α} {t₀ : Filter α} (h : ∀ (n : α), f n a n) :
                                                                                              Filter.Tendsto a t₀ (nhds 0)Filter.Tendsto f t₀ (nhds 1)

                                                                                              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.

                                                                                              theorem tendsto_norm_sub_self {E : Type u_6} [SeminormedAddGroup E] (x : E) :
                                                                                              Filter.Tendsto (fun (a : E) => a - x) (nhds x) (nhds 0)
                                                                                              theorem tendsto_norm_div_self {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                              Filter.Tendsto (fun (a : E) => a / x) (nhds x) (nhds 0)
                                                                                              theorem tendsto_norm {E : Type u_6} [SeminormedAddGroup E] {x : E} :
                                                                                              Filter.Tendsto (fun (a : E) => a) (nhds x) (nhds x)
                                                                                              theorem tendsto_norm' {E : Type u_6} [SeminormedGroup E] {x : E} :
                                                                                              Filter.Tendsto (fun (a : E) => a) (nhds x) (nhds x)
                                                                                              theorem tendsto_norm_zero {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              Filter.Tendsto (fun (a : E) => a) (nhds 0) (nhds 0)
                                                                                              theorem tendsto_norm_one {E : Type u_6} [SeminormedGroup E] :
                                                                                              Filter.Tendsto (fun (a : E) => a) (nhds 1) (nhds 0)
                                                                                              theorem continuous_norm {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              Continuous fun (a : E) => a
                                                                                              theorem continuous_norm' {E : Type u_6} [SeminormedGroup E] :
                                                                                              Continuous fun (a : E) => a
                                                                                              theorem continuous_nnnorm {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              Continuous fun (a : E) => a‖₊
                                                                                              theorem continuous_nnnorm' {E : Type u_6} [SeminormedGroup E] :
                                                                                              Continuous fun (a : E) => a‖₊
                                                                                              theorem mem_closure_one_iff_norm {E : Type u_6} [SeminormedGroup E] {x : E} :
                                                                                              theorem closure_zero_eq {E : Type u_6} [SeminormedAddGroup E] :
                                                                                              closure {0} = {x : E | x = 0}
                                                                                              theorem closure_one_eq {E : Type u_6} [SeminormedGroup E] :
                                                                                              closure {1} = {x : E | x = 0}
                                                                                              theorem Filter.Tendsto.op_zero_isBoundedUnder_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
                                                                                              Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

                                                                                              A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

                                                                                              theorem Filter.Tendsto.op_one_isBoundedUnder_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
                                                                                              Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

                                                                                              A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

                                                                                              theorem Filter.Tendsto.op_zero_isBoundedUnder_le {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∀ (x : E) (y : F), op x y x * y) :
                                                                                              Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

                                                                                              A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

                                                                                              theorem Filter.Tendsto.op_one_isBoundedUnder_le {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∀ (x : E) (y : F), op x y x * y) :
                                                                                              Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

                                                                                              A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

                                                                                              theorem Filter.Tendsto.norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : αE} (h : Filter.Tendsto f l (nhds a)) :
                                                                                              Filter.Tendsto (fun (x : α) => f x) l (nhds a)
                                                                                              theorem Filter.Tendsto.norm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {a : E} {l : Filter α} {f : αE} (h : Filter.Tendsto f l (nhds a)) :
                                                                                              Filter.Tendsto (fun (x : α) => f x) l (nhds a)
                                                                                              theorem Filter.Tendsto.nnnorm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : αE} (h : Filter.Tendsto f l (nhds a)) :
                                                                                              Filter.Tendsto (fun (x : α) => f x‖₊) l (nhds a‖₊)
                                                                                              theorem Filter.Tendsto.nnnorm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {a : E} {l : Filter α} {f : αE} (h : Filter.Tendsto f l (nhds a)) :
                                                                                              Filter.Tendsto (fun (x : α) => f x‖₊) l (nhds a‖₊)
                                                                                              theorem Continuous.norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} :
                                                                                              Continuous fContinuous fun (x : α) => f x
                                                                                              theorem Continuous.norm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α]