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
                                                          @[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
                                                            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 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_2 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                  f (x - y) = f (y - x)
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) :
                                                                  f (x - x) = 0
                                                                  @[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_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_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 := }
                                                                    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.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
                                                                              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
                                                                                @[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
                                                                                        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
                                                                                        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} [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 α] {f : αE} :
                                                                                              Continuous fContinuous fun (x : α) => f x
                                                                                              theorem Continuous.nnnorm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} :
                                                                                              Continuous fContinuous fun (x : α) => f x‖₊
                                                                                              theorem Continuous.nnnorm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} :
                                                                                              Continuous fContinuous fun (x : α) => f x‖₊
                                                                                              theorem ContinuousAt.norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} {a : α} (h : ContinuousAt f a) :
                                                                                              ContinuousAt (fun (x : α) => f x) a
                                                                                              theorem ContinuousAt.norm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} {a : α} (h : ContinuousAt f a) :
                                                                                              ContinuousAt (fun (x : α) => f x) a
                                                                                              theorem ContinuousAt.nnnorm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} {a : α} (h : ContinuousAt f a) :
                                                                                              ContinuousAt (fun (x : α) => f x‖₊) a
                                                                                              theorem ContinuousAt.nnnorm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} {a : α} (h : ContinuousAt f a) :
                                                                                              ContinuousAt (fun (x : α) => f x‖₊) a
                                                                                              theorem ContinuousWithinAt.norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
                                                                                              ContinuousWithinAt (fun (x : α) => f x) s a
                                                                                              theorem ContinuousWithinAt.norm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
                                                                                              ContinuousWithinAt (fun (x : α) => f x) s a
                                                                                              theorem ContinuousWithinAt.nnnorm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
                                                                                              ContinuousWithinAt (fun (x : α) => f x‖₊) s a
                                                                                              theorem ContinuousWithinAt.nnnorm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
                                                                                              ContinuousWithinAt (fun (x : α) => f x‖₊) s a
                                                                                              theorem ContinuousOn.norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} {s : Set α} (h : ContinuousOn f s) :
                                                                                              ContinuousOn (fun (x : α) => f x) s
                                                                                              theorem ContinuousOn.norm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} {s : Set α} (h : ContinuousOn f s) :
                                                                                              ContinuousOn (fun (x : α) => f x) s
                                                                                              theorem ContinuousOn.nnnorm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : αE} {s : Set α} (h : ContinuousOn f s) :
                                                                                              ContinuousOn (fun (x : α) => f x‖₊) s
                                                                                              theorem ContinuousOn.nnnorm' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : αE} {s : Set α} (h : ContinuousOn f s) :
                                                                                              ContinuousOn (fun (x : α) => f x‖₊) s
                                                                                              theorem eventually_ne_of_tendsto_norm_atTop {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {l : Filter α} {f : αE} (h : Filter.Tendsto (fun (y : α) => f y) l Filter.atTop) (x : E) :
                                                                                              ∀ᶠ (y : α) in l, f y x

                                                                                              If ‖y‖→∞, then we can assume y≠x for any fixed x

                                                                                              theorem eventually_ne_of_tendsto_norm_atTop' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {l : Filter α} {f : αE} (h : Filter.Tendsto (fun (y : α) => f y) l Filter.atTop) (x : E) :
                                                                                              ∀ᶠ (y : α) in l, f y x

                                                                                              If ‖y‖ → ∞, then we can assume y ≠ x for any fixed x.

                                                                                              theorem SeminormedAddCommGroup.mem_closure_iff {E : Type u_6} [SeminormedAddGroup E] {s : Set E} {a : E} :
                                                                                              a closure s ∀ (ε : ), 0 < ε∃ b ∈ s, a - b < ε
                                                                                              theorem SeminormedCommGroup.mem_closure_iff {E : Type u_6} [SeminormedGroup E] {s : Set E} {a : E} :
                                                                                              a closure s ∀ (ε : ), 0 < ε∃ b ∈ s, a / b < ε
                                                                                              theorem norm_le_zero_iff' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} :
                                                                                              a 0 a = 0
                                                                                              theorem norm_le_zero_iff''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} :
                                                                                              a 0 a = 1
                                                                                              theorem norm_eq_zero' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} :
                                                                                              a = 0 a = 0
                                                                                              theorem norm_eq_zero''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} :
                                                                                              a = 0 a = 1
                                                                                              theorem norm_pos_iff' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} :
                                                                                              0 < a a 0
                                                                                              theorem norm_pos_iff''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} :
                                                                                              0 < a a 1
                                                                                              theorem SeminormedAddGroup.tendstoUniformlyOn_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedAddGroup G] {f : ικG} {s : Set κ} {l : Filter ι} :
                                                                                              TendstoUniformlyOn f 0 l s ε > 0, ∀ᶠ (i : ι) in l, xs, f i x < ε
                                                                                              theorem SeminormedGroup.tendstoUniformlyOn_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedGroup G] {f : ικG} {s : Set κ} {l : Filter ι} :
                                                                                              TendstoUniformlyOn f 1 l s ε > 0, ∀ᶠ (i : ι) in l, xs, f i x < ε
                                                                                              theorem SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedAddGroup G] {f : ικG} {l : Filter ι} {l' : Filter κ} :
                                                                                              UniformCauchySeqOnFilter f l l' TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) l'
                                                                                              theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedGroup G] {f : ικG} {l : Filter ι} {l' : Filter κ} :
                                                                                              UniformCauchySeqOnFilter f l l' TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
                                                                                              theorem SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedAddGroup G] {f : ικG} {s : Set κ} {l : Filter ι} :
                                                                                              UniformCauchySeqOn f l s TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) s
                                                                                              theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedGroup G] {f : ικG} {s : Set κ} {l : Filter ι} :
                                                                                              UniformCauchySeqOn f l s TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) s
                                                                                              theorem SeminormedAddGroup.induced.proof_1 {𝓕 : Type u_3} (E : Type u_1) (F : Type u_2) [FunLike 𝓕 E F] [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (x : E) (y : E) :
                                                                                              dist x y = x - y
                                                                                              @[reducible]
                                                                                              def SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) :

                                                                                              A group homomorphism from an AddGroup to a SeminormedAddGroup induces a SeminormedAddGroup structure on the domain.

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[reducible]
                                                                                                def SeminormedGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [Group E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) :

                                                                                                A group homomorphism from a Group to a SeminormedGroup induces a SeminormedGroup structure on the domain.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[reducible]
                                                                                                  def SeminormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [AddCommGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) :

                                                                                                  A group homomorphism from an AddCommGroup to a SeminormedAddGroup induces a SeminormedAddCommGroup structure on the domain.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    theorem SeminormedAddCommGroup.induced.proof_1 (E : Type u_1) [AddCommGroup E] (a : E) (b : E) :
                                                                                                    a + b = b + a
                                                                                                    @[reducible]
                                                                                                    def SeminormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [CommGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) :

                                                                                                    A group homomorphism from a CommGroup to a SeminormedGroup induces a SeminormedCommGroup structure on the domain.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[reducible]
                                                                                                      def NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [AddGroup E] [NormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective f) :

                                                                                                      An injective group homomorphism from an AddGroup to a NormedAddGroup induces a NormedAddGroup structure on the domain.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[reducible]
                                                                                                        def NormedGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [Group E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective f) :

                                                                                                        An injective group homomorphism from a Group to a NormedGroup induces a NormedGroup structure on the domain.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          theorem NormedAddCommGroup.induced.proof_1 (E : Type u_1) [AddCommGroup E] (a : E) (b : E) :
                                                                                                          a + b = b + a
                                                                                                          @[reducible]
                                                                                                          def NormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [AddCommGroup E] [NormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective f) :

                                                                                                          An injective group homomorphism from a CommGroup to a NormedCommGroup induces a NormedCommGroup structure on the domain.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[reducible]
                                                                                                            def NormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [FunLike 𝓕 E F] [CommGroup E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective f) :

                                                                                                            An injective group homomorphism from a CommGroup to a NormedGroup induces a NormedCommGroup structure on the domain.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              theorem dist_neg {E : Type u_6} [SeminormedAddCommGroup E] (x : E) (y : E) :
                                                                                                              dist (-x) y = dist x (-y)
                                                                                                              theorem dist_inv {E : Type u_6} [SeminormedCommGroup E] (x : E) (y : E) :
                                                                                                              @[simp]
                                                                                                              theorem dist_self_add_right {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) :
                                                                                                              dist a (a + b) = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_mul_right {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) :
                                                                                                              dist a (a * b) = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_add_left {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) :
                                                                                                              dist (a + b) a = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_mul_left {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) :
                                                                                                              dist (a * b) a = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_sub_right {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) :
                                                                                                              dist a (a - b) = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_div_right {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) :
                                                                                                              dist a (a / b) = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_sub_left {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) :
                                                                                                              dist (a - b) a = b
                                                                                                              @[simp]
                                                                                                              theorem dist_self_div_left {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) :
                                                                                                              dist (a / b) a = b
                                                                                                              theorem dist_add_add_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              dist (a₁ + a₂) (b₁ + b₂) dist a₁ b₁ + dist a₂ b₂
                                                                                                              theorem dist_mul_mul_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              dist (a₁ * a₂) (b₁ * b₂) dist a₁ b₁ + dist a₂ b₂
                                                                                                              theorem dist_add_add_le_of_le {E : Type u_6} [SeminormedAddCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
                                                                                                              dist (a₁ + a₂) (b₁ + b₂) r₁ + r₂
                                                                                                              theorem dist_mul_mul_le_of_le {E : Type u_6} [SeminormedCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
                                                                                                              dist (a₁ * a₂) (b₁ * b₂) r₁ + r₂
                                                                                                              theorem dist_sub_sub_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              dist (a₁ - a₂) (b₁ - b₂) dist a₁ b₁ + dist a₂ b₂
                                                                                                              theorem dist_div_div_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              dist (a₁ / a₂) (b₁ / b₂) dist a₁ b₁ + dist a₂ b₂
                                                                                                              theorem dist_sub_sub_le_of_le {E : Type u_6} [SeminormedAddCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
                                                                                                              dist (a₁ - a₂) (b₁ - b₂) r₁ + r₂
                                                                                                              theorem dist_div_div_le_of_le {E : Type u_6} [SeminormedCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
                                                                                                              dist (a₁ / a₂) (b₁ / b₂) r₁ + r₂
                                                                                                              theorem abs_dist_sub_le_dist_add_add {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              |dist a₁ b₁ - dist a₂ b₂| dist (a₁ + a₂) (b₁ + b₂)
                                                                                                              theorem abs_dist_sub_le_dist_mul_mul {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              |dist a₁ b₁ - dist a₂ b₂| dist (a₁ * a₂) (b₁ * b₂)
                                                                                                              theorem norm_sum_le {ι : Type u_9} {E : Type u_10} [SeminormedAddCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                              Finset.sum s fun (i : ι) => f i Finset.sum s fun (i : ι) => f i
                                                                                                              theorem norm_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                              Finset.prod s fun (i : ι) => f i Finset.sum s fun (i : ι) => f i
                                                                                                              theorem norm_sum_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) {f : ιE} {n : ι} (h : bs, f b n b) :
                                                                                                              Finset.sum s fun (b : ι) => f b Finset.sum s fun (b : ι) => n b
                                                                                                              theorem norm_prod_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) {f : ιE} {n : ι} (h : bs, f b n b) :
                                                                                                              Finset.prod s fun (b : ι) => f b Finset.sum s fun (b : ι) => n b
                                                                                                              theorem dist_sum_sum_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) {f : ιE} {a : ιE} {d : ι} (h : bs, dist (f b) (a b) d b) :
                                                                                                              dist (Finset.sum s fun (b : ι) => f b) (Finset.sum s fun (b : ι) => a b) Finset.sum s fun (b : ι) => d b
                                                                                                              theorem dist_prod_prod_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) {f : ιE} {a : ιE} {d : ι} (h : bs, dist (f b) (a b) d b) :
                                                                                                              dist (Finset.prod s fun (b : ι) => f b) (Finset.prod s fun (b : ι) => a b) Finset.sum s fun (b : ι) => d b
                                                                                                              theorem dist_sum_sum_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) (f : ιE) (a : ιE) :
                                                                                                              dist (Finset.sum s fun (b : ι) => f b) (Finset.sum s fun (b : ι) => a b) Finset.sum s fun (b : ι) => dist (f b) (a b)
                                                                                                              theorem dist_prod_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ιE) (a : ιE) :
                                                                                                              dist (Finset.prod s fun (b : ι) => f b) (Finset.prod s fun (b : ι) => a b) Finset.sum s fun (b : ι) => dist (f b) (a b)
                                                                                                              theorem add_mem_ball_iff_norm {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem mul_mem_ball_iff_norm {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem add_mem_closedBall_iff_norm {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem mul_mem_closedBall_iff_norm {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              @[simp]
                                                                                                              theorem preimage_add_ball {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) (r : ) :
                                                                                                              (fun (x : E) => b + x) ⁻¹' Metric.ball a r = Metric.ball (a - b) r
                                                                                                              @[simp]
                                                                                                              theorem preimage_mul_ball {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) (r : ) :
                                                                                                              (fun (x : E) => b * x) ⁻¹' Metric.ball a r = Metric.ball (a / b) r
                                                                                                              @[simp]
                                                                                                              theorem preimage_add_closedBall {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) (r : ) :
                                                                                                              (fun (x : E) => b + x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a - b) r
                                                                                                              @[simp]
                                                                                                              theorem preimage_mul_closedBall {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) (r : ) :
                                                                                                              (fun (x : E) => b * x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a / b) r
                                                                                                              @[simp]
                                                                                                              theorem preimage_add_sphere {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) (r : ) :
                                                                                                              (fun (x : E) => b + x) ⁻¹' Metric.sphere a r = Metric.sphere (a - b) r
                                                                                                              @[simp]
                                                                                                              theorem preimage_mul_sphere {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) (r : ) :
                                                                                                              (fun (x : E) => b * x) ⁻¹' Metric.sphere a r = Metric.sphere (a / b) r
                                                                                                              theorem norm_nsmul_le {E : Type u_6} [SeminormedAddCommGroup E] (n : ) (a : E) :
                                                                                                              n a n * a
                                                                                                              theorem norm_pow_le_mul_norm {E : Type u_6} [SeminormedCommGroup E] (n : ) (a : E) :
                                                                                                              a ^ n n * a
                                                                                                              theorem nnnorm_nsmul_le {E : Type u_6} [SeminormedAddCommGroup E] (n : ) (a : E) :
                                                                                                              theorem nnnorm_pow_le_mul_norm {E : Type u_6} [SeminormedCommGroup E] (n : ) (a : E) :
                                                                                                              theorem nsmul_mem_closedBall {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } {n : } (h : a Metric.closedBall b r) :
                                                                                                              n a Metric.closedBall (n b) (n r)
                                                                                                              theorem pow_mem_closedBall {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } {n : } (h : a Metric.closedBall b r) :
                                                                                                              a ^ n Metric.closedBall (b ^ n) (n r)
                                                                                                              theorem nsmul_mem_ball {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } {n : } (hn : 0 < n) (h : a Metric.ball b r) :
                                                                                                              n a Metric.ball (n b) (n r)
                                                                                                              theorem pow_mem_ball {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } {n : } (hn : 0 < n) (h : a Metric.ball b r) :
                                                                                                              a ^ n Metric.ball (b ^ n) (n r)
                                                                                                              theorem add_mem_closedBall_add_iff {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } {c : E} :
                                                                                                              theorem mul_mem_closedBall_mul_iff {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } {c : E} :
                                                                                                              theorem add_mem_ball_add_iff {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } {c : E} :
                                                                                                              a + c Metric.ball (b + c) r a Metric.ball b r
                                                                                                              theorem mul_mem_ball_mul_iff {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } {c : E} :
                                                                                                              a * c Metric.ball (b * c) r a Metric.ball b r
                                                                                                              theorem vadd_closedBall'' {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem smul_closedBall'' {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem vadd_ball'' {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem smul_ball'' {E : Type u_6} [SeminormedCommGroup E] {a : E} {b : E} {r : } :
                                                                                                              theorem controlled_sum_of_mem_closure {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {s : AddSubgroup E} (hg : a closure s) {b : } (b_pos : ∀ (n : ), 0 < b n) :
                                                                                                              ∃ (v : E), Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range (n + 1)) fun (i : ) => v i) Filter.atTop (nhds a) (∀ (n : ), v n s) v 0 - a < b 0 ∀ (n : ), 0 < nv n < b n
                                                                                                              theorem controlled_prod_of_mem_closure {E : Type u_6} [SeminormedCommGroup E] {a : E} {s : Subgroup E} (hg : a closure s) {b : } (b_pos : ∀ (n : ), 0 < b n) :
                                                                                                              ∃ (v : E), Filter.Tendsto (fun (n : ) => Finset.prod (Finset.range (n + 1)) fun (i : ) => v i) Filter.atTop (nhds a) (∀ (n : ), v n s) v 0 / a < b 0 ∀ (n : ), 0 < nv n < b n
                                                                                                              theorem controlled_sum_of_mem_closure_range {E : Type u_6} {F : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {j : E →+ F} {b : F} (hb : b closure (AddMonoidHom.range j)) {f : } (b_pos : ∀ (n : ), 0 < f n) :
                                                                                                              ∃ (a : E), Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range (n + 1)) fun (i : ) => j (a i)) Filter.atTop (nhds b) j (a 0) - b < f 0 ∀ (n : ), 0 < nj (a n) < f n
                                                                                                              theorem controlled_prod_of_mem_closure_range {E : Type u_6} {F : Type u_7} [SeminormedCommGroup E] [SeminormedCommGroup F] {j : E →* F} {b : F} (hb : b closure (MonoidHom.range j)) {f : } (b_pos : ∀ (n : ), 0 < f n) :
                                                                                                              ∃ (a : E), Filter.Tendsto (fun (n : ) => Finset.prod (Finset.range (n + 1)) fun (i : ) => j (a i)) Filter.atTop (nhds b) j (a 0) / b < f 0 ∀ (n : ), 0 < nj (a n) < f n
                                                                                                              theorem nndist_add_add_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              nndist (a₁ + a₂) (b₁ + b₂) nndist a₁ b₁ + nndist a₂ b₂
                                                                                                              theorem nndist_mul_mul_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              nndist (a₁ * a₂) (b₁ * b₂) nndist a₁ b₁ + nndist a₂ b₂
                                                                                                              theorem edist_add_add_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              edist (a₁ + a₂) (b₁ + b₂) edist a₁ b₁ + edist a₂ b₂
                                                                                                              theorem edist_mul_mul_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
                                                                                                              edist (a₁ * a₂) (b₁ * b₂) edist a₁ b₁ + edist a₂ b₂
                                                                                                              theorem nnnorm_sum_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                              Finset.sum s fun (a : ι) => f a‖₊ Finset.sum s fun (a : ι) => f a‖₊
                                                                                                              theorem nnnorm_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                              Finset.prod s fun (a : ι) => f a‖₊ Finset.sum s fun (a : ι) => f a‖₊
                                                                                                              theorem nnnorm_sum_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) {f : ιE} {n : ιNNReal} (h : bs, f b‖₊ n b) :
                                                                                                              Finset.sum s fun (b : ι) => f b‖₊ Finset.sum s fun (b : ι) => n b
                                                                                                              theorem nnnorm_prod_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) {f : ιE} {n : ιNNReal} (h : bs, f b‖₊ n b) :
                                                                                                              Finset.prod s fun (b : ι) => f b‖₊ Finset.sum s fun (b : ι) => n b
                                                                                                              instance Real.norm :
                                                                                                              Equations
                                                                                                              @[simp]
                                                                                                              theorem Real.norm_eq_abs (r : ) :
                                                                                                              r = |r|
                                                                                                              theorem Real.norm_of_nonneg {r : } (hr : 0 r) :
                                                                                                              theorem Real.norm_of_nonpos {r : } (hr : r 0) :
                                                                                                              theorem Real.norm_coe_nat (n : ) :
                                                                                                              n = n
                                                                                                              @[simp]
                                                                                                              theorem Real.nnnorm_coe_nat (n : ) :
                                                                                                              n‖₊ = n
                                                                                                              @[simp]
                                                                                                              theorem Real.nnnorm_of_nonneg {r : } (hr : 0 r) :
                                                                                                              r‖₊ = { val := r, property := hr }
                                                                                                              @[simp]
                                                                                                              theorem Int.norm_eq_abs (n : ) :
                                                                                                              n = |n|
                                                                                                              @[simp]
                                                                                                              theorem Int.norm_coe_nat (n : ) :
                                                                                                              n = n
                                                                                                              @[simp]
                                                                                                              theorem Rat.norm_cast_real (r : ) :
                                                                                                              @[simp]
                                                                                                              theorem Int.norm_cast_rat (m : ) :
                                                                                                              theorem norm_zsmul_le {α : Type u_3} [SeminormedAddCommGroup α] (n : ) (a : α) :
                                                                                                              theorem norm_zpow_le_mul_norm {α : Type u_3} [SeminormedCommGroup α] (n : ) (a : α) :
                                                                                                              theorem LipschitzWith.neg {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} (hf : LipschitzWith K f) :
                                                                                                              LipschitzWith K fun (x : α) => -f x
                                                                                                              theorem LipschitzWith.inv {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} (hf : LipschitzWith K f) :
                                                                                                              LipschitzWith K fun (x : α) => (f x)⁻¹
                                                                                                              theorem LipschitzWith.add {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
                                                                                                              LipschitzWith (Kf + Kg) fun (x : α) => f x + g x
                                                                                                              theorem LipschitzWith.mul' {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
                                                                                                              LipschitzWith (Kf + Kg) fun (x : α) => f x * g x
                                                                                                              theorem LipschitzWith.sub {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
                                                                                                              LipschitzWith (Kf + Kg) fun (x : α) => f x - g x
                                                                                                              theorem LipschitzWith.div {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
                                                                                                              LipschitzWith (Kf + Kg) fun (x : α) => f x / g x
                                                                                                              theorem AntilipschitzWith.add_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) :
                                                                                                              AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x + g x
                                                                                                              theorem AntilipschitzWith.mul_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) :
                                                                                                              AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x * g x
                                                                                                              theorem AntilipschitzWith.add_sub_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g - f)) (hK : Kg < Kf⁻¹) :
                                                                                                              theorem AntilipschitzWith.mul_div_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) :
                                                                                                              theorem AntilipschitzWith.le_mul_norm_sub {E : Type u_6} {F : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {K : NNReal} {f : EF} (hf : AntilipschitzWith K f) (x : E) (y : E) :
                                                                                                              x - y K * f x - f y
                                                                                                              theorem AntilipschitzWith.le_mul_norm_div {E : Type u_6} {F : Type u_7} [SeminormedCommGroup E] [SeminormedCommGroup F] {K : NNReal} {f : EF} (hf : AntilipschitzWith K f) (x : E) (y : E) :
                                                                                                              x / y K * f x / f y

                                                                                                              A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

                                                                                                              Equations
                                                                                                              • =

                                                                                                              A seminormed group is a uniform group, i.e., multiplication and division are uniformly continuous.

                                                                                                              Equations
                                                                                                              • =
                                                                                                              theorem cauchySeq_sum_of_eventually_eq {E : Type u_6} [SeminormedAddCommGroup E] {u : E} {v : E} {N : } (huv : nN, u n = v n) (hv : CauchySeq fun (n : ) => Finset.sum (Finset.range (n + 1)) fun (k : ) => v k) :
                                                                                                              CauchySeq fun (n : ) => Finset.sum (Finset.range (n + 1)) fun (k : ) => u k
                                                                                                              theorem cauchySeq_prod_of_eventually_eq {E : Type u_6} [SeminormedCommGroup E] {u : E} {v : E} {N : } (huv : nN, u n = v n) (hv : CauchySeq fun (n : ) => Finset.prod (Finset.range (n + 1)) fun (k : ) => v k) :
                                                                                                              CauchySeq fun (n : ) => Finset.prod (Finset.range (n + 1)) fun (k : ) => u k
                                                                                                              @[simp]
                                                                                                              theorem norm_eq_zero {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              a = 0 a = 0
                                                                                                              @[simp]
                                                                                                              theorem norm_eq_zero'' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              a = 0 a = 1
                                                                                                              theorem norm_ne_zero_iff {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              a 0 a 0
                                                                                                              theorem norm_ne_zero_iff' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              a 0 a 1
                                                                                                              @[simp]
                                                                                                              theorem norm_pos_iff {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              0 < a a 0
                                                                                                              @[simp]
                                                                                                              theorem norm_pos_iff'' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              0 < a a 1
                                                                                                              @[simp]
                                                                                                              theorem norm_le_zero_iff {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              a 0 a = 0
                                                                                                              @[simp]
                                                                                                              theorem norm_le_zero_iff'' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              a 0 a = 1
                                                                                                              theorem norm_sub_eq_zero_iff {E : Type u_6} [NormedAddGroup E] {a : E} {b : E} :
                                                                                                              a - b = 0 a = b
                                                                                                              theorem norm_div_eq_zero_iff {E : Type u_6} [NormedGroup E] {a : E} {b : E} :
                                                                                                              a / b = 0 a = b
                                                                                                              theorem norm_sub_pos_iff {E : Type u_6} [NormedAddGroup E] {a : E} {b : E} :
                                                                                                              0 < a - b a b
                                                                                                              theorem norm_div_pos_iff {E : Type u_6} [NormedGroup E] {a : E} {b : E} :
                                                                                                              0 < a / b a b
                                                                                                              theorem eq_of_norm_sub_le_zero {E : Type u_6} [NormedAddGroup E] {a : E} {b : E} (h : a - b 0) :
                                                                                                              a = b
                                                                                                              theorem eq_of_norm_div_le_zero {E : Type u_6} [NormedGroup E] {a : E} {b : E} (h : a / b 0) :
                                                                                                              a = b
                                                                                                              theorem eq_of_norm_div_eq_zero {E : Type u_6} [NormedGroup E] {a : E} {b : E} :
                                                                                                              a / b = 0a = b

                                                                                                              Alias of the forward direction of norm_div_eq_zero_iff.

                                                                                                              theorem eq_of_norm_sub_eq_zero {E : Type u_6} [NormedAddGroup E] {a : E} {b : E} :
                                                                                                              a - b = 0a = b
                                                                                                              @[simp]
                                                                                                              theorem nnnorm_eq_zero {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              a‖₊ = 0 a = 0
                                                                                                              @[simp]
                                                                                                              theorem nnnorm_eq_zero' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              a‖₊ = 0 a = 1
                                                                                                              theorem nnnorm_ne_zero_iff {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              theorem nnnorm_ne_zero_iff' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              @[simp]
                                                                                                              theorem nnnorm_pos {E : Type u_6} [NormedAddGroup E] {a : E} :
                                                                                                              @[simp]
                                                                                                              theorem nnnorm_pos' {E : Type u_6} [NormedGroup E] {a : E} :
                                                                                                              theorem tendsto_norm_sub_self_punctured_nhds {E : Type u_6} [NormedAddGroup E] (a : E) :
                                                                                                              Filter.Tendsto (fun (x : E) => x - a) (nhdsWithin a {a}) (nhdsWithin 0 (Set.Ioi 0))
                                                                                                              theorem tendsto_norm_div_self_punctured_nhds {E : Type u_6} [NormedGroup E] (a : E) :
                                                                                                              Filter.Tendsto (fun (x : E) => x / a) (nhdsWithin a {a}) (nhdsWithin 0 (Set.Ioi 0))
                                                                                                              theorem normAddGroupNorm.proof_1 (E : Type u_1) [NormedAddGroup E] :
                                                                                                              ∀ (x : E), x = 0x = 0

                                                                                                              The norm of a normed group as an additive group norm.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                The norm of a normed group as a group norm.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem coe_normGroupNorm (E : Type u_6) [NormedGroup E] :
                                                                                                                  (normGroupNorm E) = norm

                                                                                                                  Some relations with HasCompactSupport

                                                                                                                  theorem hasCompactSupport_norm_iff {α : Type u_3} {E : Type u_6} [NormedAddGroup E] [TopologicalSpace α] {f : αE} :
                                                                                                                  theorem HasCompactSupport.norm {α : Type u_3} {E : Type u_6} [NormedAddGroup E] [TopologicalSpace α] {f : αE} :
                                                                                                                  HasCompactSupport fHasCompactSupport fun (x : α) => f x

                                                                                                                  Alias of the reverse direction of hasCompactSupport_norm_iff.

                                                                                                                  theorem Continuous.bounded_above_of_compact_support {α : Type u_3} {E : Type u_6} [NormedAddGroup E] [TopologicalSpace α] {f : αE} (hf : Continuous f) (h : HasCompactSupport f) :
                                                                                                                  ∃ (C : ), ∀ (x : α), f x C
                                                                                                                  theorem HasCompactSupport.exists_pos_le_norm {α : Type u_3} {E : Type u_6} [NormedAddGroup α] {f : αE} [Zero E] (hf : HasCompactSupport f) :
                                                                                                                  ∃ (R : ), 0 < R ∀ (x : α), R xf x = 0
                                                                                                                  theorem HasCompactMulSupport.exists_pos_le_norm {α : Type u_3} {E : Type u_6} [NormedAddGroup α] {f : αE} [One E] (hf : HasCompactMulSupport f) :
                                                                                                                  ∃ (R : ), 0 < R ∀ (x : α), R xf x = 1

                                                                                                                  ULift #

                                                                                                                  instance ULift.norm {E : Type u_6} [Norm E] :
                                                                                                                  Equations
                                                                                                                  theorem ULift.norm_def {E : Type u_6} [Norm E] (x : ULift.{u_9, u_6} E) :
                                                                                                                  x = x.down
                                                                                                                  @[simp]
                                                                                                                  theorem ULift.norm_up {E : Type u_6} [Norm E] (x : E) :
                                                                                                                  { down := x } = x
                                                                                                                  @[simp]
                                                                                                                  theorem ULift.norm_down {E : Type u_6} [Norm E] (x : ULift.{u_9, u_6} E) :
                                                                                                                  x.down = x
                                                                                                                  instance ULift.nnnorm {E : Type u_6} [NNNorm E] :
                                                                                                                  Equations
                                                                                                                  @[simp]
                                                                                                                  theorem ULift.nnnorm_up {E : Type u_6} [NNNorm E] (x : E) :
                                                                                                                  { down := x }‖₊ = x‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem ULift.nnnorm_down {E : Type u_6} [NNNorm E] (x : ULift.{u_9, u_6} E) :
                                                                                                                  Equations
                                                                                                                  theorem ULift.seminormedAddGroup.proof_3 {E : Type u_2} [SeminormedAddGroup E] :
                                                                                                                  ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := }.toFun (x + x_1)
                                                                                                                  Equations
                                                                                                                  theorem ULift.seminormedAddCommGroup.proof_3 {E : Type u_2} [SeminormedAddCommGroup E] :
                                                                                                                  ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := }.toFun (x + x_1)
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  theorem ULift.normedAddGroup.proof_3 {E : Type u_2} [NormedAddGroup E] :
                                                                                                                  ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := }.toFun (x + x_1)
                                                                                                                  theorem ULift.normedAddGroup.proof_2 {E : Type u_1} [NormedAddGroup E] :
                                                                                                                  0.down = 0.down
                                                                                                                  Equations
                                                                                                                  theorem ULift.normedAddCommGroup.proof_3 {E : Type u_2} [NormedAddCommGroup E] :
                                                                                                                  ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := }.toFun (x + x_1)
                                                                                                                  Equations
                                                                                                                  Equations

                                                                                                                  Additive, Multiplicative #

                                                                                                                  instance Additive.toNorm {E : Type u_6} [Norm E] :
                                                                                                                  Equations
                                                                                                                  • Additive.toNorm = inst
                                                                                                                  instance Multiplicative.toNorm {E : Type u_6} [Norm E] :
                                                                                                                  Equations
                                                                                                                  • Multiplicative.toNorm = inst
                                                                                                                  @[simp]
                                                                                                                  theorem norm_toMul {E : Type u_6} [Norm E] (x : Additive E) :
                                                                                                                  Additive.toMul x = x
                                                                                                                  @[simp]
                                                                                                                  theorem norm_ofMul {E : Type u_6} [Norm E] (x : E) :
                                                                                                                  Additive.ofMul x = x
                                                                                                                  @[simp]
                                                                                                                  theorem norm_toAdd {E : Type u_6} [Norm E] (x : Multiplicative E) :
                                                                                                                  Multiplicative.toAdd x = x
                                                                                                                  @[simp]
                                                                                                                  theorem norm_ofAdd {E : Type u_6} [Norm E] (x : E) :
                                                                                                                  Multiplicative.ofAdd x = x
                                                                                                                  instance Additive.toNNNorm {E : Type u_6} [NNNorm E] :
                                                                                                                  Equations
                                                                                                                  • Additive.toNNNorm = inst
                                                                                                                  Equations
                                                                                                                  • Multiplicative.toNNNorm = inst
                                                                                                                  @[simp]
                                                                                                                  theorem nnnorm_toMul {E : Type u_6} [NNNorm E] (x : Additive E) :
                                                                                                                  Additive.toMul x‖₊ = x‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem nnnorm_ofMul {E : Type u_6} [NNNorm E] (x : E) :
                                                                                                                  Additive.ofMul x‖₊ = x‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem nnnorm_toAdd {E : Type u_6} [NNNorm E] (x : Multiplicative E) :
                                                                                                                  Multiplicative.toAdd x‖₊ = x‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem nnnorm_ofAdd {E : Type u_6} [NNNorm E] (x : E) :
                                                                                                                  Multiplicative.ofAdd x‖₊ = x‖₊
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  • Multiplicative.normedGroup = let __src := Multiplicative.seminormedGroup; NormedGroup.mk
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  • Multiplicative.normedCommGroup = let __src := Multiplicative.seminormedGroup; NormedCommGroup.mk

                                                                                                                  Order dual #

                                                                                                                  instance OrderDual.toNorm {E : Type u_6} [Norm E] :
                                                                                                                  Equations
                                                                                                                  • OrderDual.toNorm = inst
                                                                                                                  @[simp]
                                                                                                                  theorem norm_toDual {E : Type u_6} [Norm E] (x : E) :
                                                                                                                  OrderDual.toDual x = x
                                                                                                                  @[simp]
                                                                                                                  theorem norm_ofDual {E : Type u_6} [Norm E] (x : Eᵒᵈ) :
                                                                                                                  OrderDual.ofDual x = x
                                                                                                                  instance OrderDual.toNNNorm {E : Type u_6} [NNNorm E] :
                                                                                                                  Equations
                                                                                                                  • OrderDual.toNNNorm = inst
                                                                                                                  @[simp]
                                                                                                                  theorem nnnorm_toDual {E : Type u_6} [NNNorm E] (x : E) :
                                                                                                                  OrderDual.toDual x‖₊ = x‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem nnnorm_ofDual {E : Type u_6} [NNNorm E] (x : Eᵒᵈ) :
                                                                                                                  OrderDual.ofDual x‖₊ = x‖₊
                                                                                                                  Equations
                                                                                                                  • OrderDual.seminormedAddGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.seminormedGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.seminormedAddCommGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.seminormedCommGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.normedAddGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.normedGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.normedAddCommGroup = inst
                                                                                                                  Equations
                                                                                                                  • OrderDual.normedCommGroup = inst

                                                                                                                  Binary product of normed groups #

                                                                                                                  instance Prod.toNorm {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] :
                                                                                                                  Norm (E × F)
                                                                                                                  Equations
                                                                                                                  theorem Prod.norm_def {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (x : E × F) :
                                                                                                                  theorem norm_fst_le {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (x : E × F) :
                                                                                                                  theorem norm_snd_le {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (x : E × F) :
                                                                                                                  theorem norm_prod_le_iff {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] {x : E × F} {r : } :
                                                                                                                  theorem Prod.seminormedAddGroup.proof_1 {E : Type u_1} {F : Type u_2} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E × F) (y : E × F) :
                                                                                                                  max (dist x.1 y.1) (dist x.2 y.2) = max x.1 - y.1 x.2 - y.2

                                                                                                                  Product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  instance Prod.seminormedGroup {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] :

                                                                                                                  Product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Prod.nnorm_def {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] (x : E × F) :
                                                                                                                  theorem Prod.seminormedAddCommGroup.proof_2 {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (x : E × F) (y : E × F) :
                                                                                                                  dist x y = x - y

                                                                                                                  Product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Prod.seminormedAddCommGroup.proof_1 {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (a : E × F) (b : E × F) :
                                                                                                                  a + b = b + a

                                                                                                                  Product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Prod.normedAddGroup.proof_2 {E : Type u_1} {F : Type u_2} [NormedAddGroup E] [NormedAddGroup F] (x : E × F) (y : E × F) :
                                                                                                                  dist x y = x - y
                                                                                                                  theorem Prod.normedAddGroup.proof_1 {E : Type u_1} {F : Type u_2} [NormedAddGroup E] [NormedAddGroup F] :
                                                                                                                  ∀ {x y : E × F}, dist x y = 0x = y
                                                                                                                  instance Prod.normedAddGroup {E : Type u_6} {F : Type u_7} [NormedAddGroup E] [NormedAddGroup F] :

                                                                                                                  Product of normed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  instance Prod.normedGroup {E : Type u_6} {F : Type u_7} [NormedGroup E] [NormedGroup F] :

                                                                                                                  Product of normed groups, using the sup norm.

                                                                                                                  Equations

                                                                                                                  Product of normed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Prod.normedAddCommGroup.proof_1 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (a : E × F) (b : E × F) :
                                                                                                                  a + b = b + a
                                                                                                                  theorem Prod.normedAddCommGroup.proof_2 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] :
                                                                                                                  ∀ {x y : E × F}, dist x y = 0x = y
                                                                                                                  theorem Prod.normedAddCommGroup.proof_3 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (x : E × F) (y : E × F) :
                                                                                                                  dist x y = x - y
                                                                                                                  instance Prod.normedCommGroup {E : Type u_6} {F : Type u_7} [NormedCommGroup E] [NormedCommGroup F] :

                                                                                                                  Product of normed groups, using the sup norm.

                                                                                                                  Equations

                                                                                                                  Finite product of normed groups #

                                                                                                                  theorem Pi.seminormedAddGroup.proof_1 {ι : Type u_1} {π : ιType u_2} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :
                                                                                                                  (Finset.sup Finset.univ fun (b : ι) => nndist (x b) (y b)) = (Finset.sup Finset.univ fun (b : ι) => (x - y) b‖₊)
                                                                                                                  instance Pi.seminormedAddGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] :
                                                                                                                  SeminormedAddGroup ((i : ι) → π i)

                                                                                                                  Finite product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  instance Pi.seminormedGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] :
                                                                                                                  SeminormedGroup ((i : ι) → π i)

                                                                                                                  Finite product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Pi.norm_def {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  f = (Finset.sup Finset.univ fun (b : ι) => f b‖₊)
                                                                                                                  theorem Pi.norm_def' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  f = (Finset.sup Finset.univ fun (b : ι) => f b‖₊)
                                                                                                                  theorem Pi.nnnorm_def {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  f‖₊ = Finset.sup Finset.univ fun (b : ι) => f b‖₊
                                                                                                                  theorem Pi.nnnorm_def' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  f‖₊ = Finset.sup Finset.univ fun (b : ι) => f b‖₊
                                                                                                                  theorem pi_norm_le_iff_of_nonneg {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : } (hr : 0 r) :
                                                                                                                  x r ∀ (i : ι), x i r

                                                                                                                  The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

                                                                                                                  theorem pi_norm_le_iff_of_nonneg' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : } (hr : 0 r) :
                                                                                                                  x r ∀ (i : ι), x i r

                                                                                                                  The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

                                                                                                                  theorem pi_nnnorm_le_iff {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : NNReal} :
                                                                                                                  x‖₊ r ∀ (i : ι), x i‖₊ r
                                                                                                                  theorem pi_nnnorm_le_iff' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : NNReal} :
                                                                                                                  x‖₊ r ∀ (i : ι), x i‖₊ r
                                                                                                                  theorem pi_norm_le_iff_of_nonempty {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) {r : } [Nonempty ι] :
                                                                                                                  f r ∀ (b : ι), f b r
                                                                                                                  theorem pi_norm_le_iff_of_nonempty' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) {r : } [Nonempty ι] :
                                                                                                                  f r ∀ (b : ι), f b r
                                                                                                                  theorem pi_norm_lt_iff {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : } (hr : 0 < r) :
                                                                                                                  x < r ∀ (i : ι), x i < r

                                                                                                                  The seminorm of an element in a product space is < r if and only if the norm of each component is.

                                                                                                                  theorem pi_norm_lt_iff' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : } (hr : 0 < r) :
                                                                                                                  x < r ∀ (i : ι), x i < r

                                                                                                                  The seminorm of an element in a product space is < r if and only if the norm of each component is.

                                                                                                                  theorem pi_nnnorm_lt_iff {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : NNReal} (hr : 0 < r) :
                                                                                                                  x‖₊ < r ∀ (i : ι), x i‖₊ < r
                                                                                                                  theorem pi_nnnorm_lt_iff' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : NNReal} (hr : 0 < r) :
                                                                                                                  x‖₊ < r ∀ (i : ι), x i‖₊ < r
                                                                                                                  theorem norm_le_pi_norm {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) (i : ι) :
                                                                                                                  theorem norm_le_pi_norm' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) (i : ι) :
                                                                                                                  theorem nnnorm_le_pi_nnnorm {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) (i : ι) :
                                                                                                                  theorem nnnorm_le_pi_nnnorm' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) (i : ι) :
                                                                                                                  theorem pi_norm_const_le {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] (a : E) :
                                                                                                                  fun (x : ι) => a a
                                                                                                                  theorem pi_norm_const_le' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] (a : E) :
                                                                                                                  fun (x : ι) => a a
                                                                                                                  theorem pi_nnnorm_const_le {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] (a : E) :
                                                                                                                  fun (x : ι) => a‖₊ a‖₊
                                                                                                                  theorem pi_nnnorm_const_le' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] (a : E) :
                                                                                                                  fun (x : ι) => a‖₊ a‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem pi_norm_const {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) :
                                                                                                                  fun (_i : ι) => a = a
                                                                                                                  @[simp]
                                                                                                                  theorem pi_norm_const' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) :
                                                                                                                  fun (_i : ι) => a = a
                                                                                                                  @[simp]
                                                                                                                  theorem pi_nnnorm_const {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) :
                                                                                                                  fun (_i : ι) => a‖₊ = a‖₊
                                                                                                                  @[simp]
                                                                                                                  theorem pi_nnnorm_const' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) :
                                                                                                                  fun (_i : ι) => a‖₊ = a‖₊
                                                                                                                  theorem Pi.sum_norm_apply_le_norm {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  (Finset.sum Finset.univ fun (i : ι) => f i) Fintype.card ι f

                                                                                                                  The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                                                                                  theorem Pi.sum_norm_apply_le_norm' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  (Finset.sum Finset.univ fun (i : ι) => f i) Fintype.card ι f

                                                                                                                  The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                                                                                  theorem Pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  (Finset.sum Finset.univ fun (i : ι) => f i‖₊) Fintype.card ι f‖₊

                                                                                                                  The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                                                                                  theorem Pi.sum_nnnorm_apply_le_nnnorm' {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) :
                                                                                                                  (Finset.sum Finset.univ fun (i : ι) => f i‖₊) Fintype.card ι f‖₊

                                                                                                                  The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                                                                                  instance Pi.seminormedAddCommGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (π i)] :
                                                                                                                  SeminormedAddCommGroup ((i : ι) → π i)

                                                                                                                  Finite product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Pi.seminormedAddCommGroup.proof_1 {ι : Type u_1} {π : ιType u_2} [(i : ι) → SeminormedAddCommGroup (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :
                                                                                                                  a + b = b + a
                                                                                                                  theorem Pi.seminormedAddCommGroup.proof_2 {ι : Type u_1} {π : ιType u_2} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :
                                                                                                                  dist x y = x - y
                                                                                                                  instance Pi.seminormedCommGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → SeminormedCommGroup (π i)] :
                                                                                                                  SeminormedCommGroup ((i : ι) → π i)

                                                                                                                  Finite product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Pi.normedAddGroup.proof_1 {ι : Type u_1} {π : ιType u_2} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] :
                                                                                                                  ∀ {x y : (i : ι) → π i}, dist x y = 0x = y
                                                                                                                  instance Pi.normedAddGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] :
                                                                                                                  NormedAddGroup ((i : ι) → π i)

                                                                                                                  Finite product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Pi.normedAddGroup.proof_2 {ι : Type u_1} {π : ιType u_2} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :
                                                                                                                  dist x y = x - y
                                                                                                                  instance Pi.normedGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → NormedGroup (π i)] :
                                                                                                                  NormedGroup ((i : ι) → π i)

                                                                                                                  Finite product of normed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Pi.normedAddCommGroup.proof_2 {ι : Type u_1} {π : ιType u_2} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] :
                                                                                                                  ∀ {x y : (i : ι) → π i}, dist x y = 0x = y
                                                                                                                  theorem Pi.normedAddCommGroup.proof_1 {ι : Type u_1} {π : ιType u_2} [(i : ι) → NormedAddCommGroup (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :
                                                                                                                  a + b = b + a
                                                                                                                  instance Pi.normedAddCommGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] :
                                                                                                                  NormedAddCommGroup ((i : ι) → π i)

                                                                                                                  Finite product of seminormed groups, using the sup norm.

                                                                                                                  Equations
                                                                                                                  theorem Pi.normedAddCommGroup.proof_3 {ι : Type u_1} {π : ιType u_2} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :
                                                                                                                  dist x y = x - y
                                                                                                                  instance Pi.normedCommGroup {ι : Type u_4} {π : ιType u_9} [Fintype ι] [(i : ι) → NormedCommGroup (π i)] :
                                                                                                                  NormedCommGroup ((i : ι) → π i)

                                                                                                                  Finite product of normed groups, using the sup norm.

                                                                                                                  Equations

                                                                                                                  Multiplicative opposite #

                                                                                                                  The (additive) norm on the multiplicative opposite is the same as the norm on the original type.

                                                                                                                  Note that we do not provide this more generally as Norm Eᵐᵒᵖ, as this is not always a good choice of norm in the multiplicative SeminormedGroup E case.

                                                                                                                  We could repeat this instance to provide a [SeminormedGroup E] : SeminormedGroup Eᵃᵒᵖ instance, but that case would likely never be used.

                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  • MulOpposite.normedAddGroup = let __src := MulOpposite.seminormedAddGroup; NormedAddGroup.mk
                                                                                                                  Equations

                                                                                                                  Subgroups of normed groups #

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

                                                                                                                  Equations

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

                                                                                                                  Equations
                                                                                                                  @[simp]
                                                                                                                  theorem AddSubgroup.coe_norm {E : Type u_6} [SeminormedAddGroup E] {s : AddSubgroup E} (x : s) :

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

                                                                                                                  @[simp]
                                                                                                                  theorem Subgroup.coe_norm {E : Type u_6} [SeminormedGroup E] {s : Subgroup E} (x : s) :

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

                                                                                                                  theorem AddSubgroup.norm_coe {E : Type u_6} [SeminormedAddGroup E] {s : AddSubgroup E} (x : s) :

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

                                                                                                                  This is a reversed version of the simp lemma AddSubgroup.coe_norm for use by norm_cast.

                                                                                                                  theorem Subgroup.norm_coe {E : Type u_6} [SeminormedGroup E] {s : Subgroup E} (x : s) :

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

                                                                                                                  This is a reversed version of the simp lemma Subgroup.coe_norm for use by norm_cast.

                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  theorem AddSubgroup.normedAddGroup.proof_2 {E : Type u_1} [NormedAddGroup E] {s : AddSubgroup E} :
                                                                                                                  Function.Injective fun (a : s) => a
                                                                                                                  instance Subgroup.normedGroup {E : Type u_6} [NormedGroup E] {s : Subgroup E} :
                                                                                                                  Equations
                                                                                                                  Equations
                                                                                                                  Equations

                                                                                                                  Submodules of normed groups #

                                                                                                                  instance Submodule.seminormedAddCommGroup {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) :

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

                                                                                                                  Equations
                                                                                                                  @[simp]
                                                                                                                  theorem Submodule.coe_norm {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : s) :

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

                                                                                                                  theorem Submodule.norm_coe {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : s) :

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

                                                                                                                  This is a reversed version of the simp lemma Submodule.coe_norm for use by norm_cast.

                                                                                                                  instance Submodule.normedAddCommGroup {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) :

                                                                                                                  A submodule of a normed group is also a normed group, with the restriction of the norm.

                                                                                                                  Equations