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
            theorem SeminormedAddGroup.dist_eq {E : Type u_9} [self : SeminormedAddGroup E] (x : E) (y : E) :
            dist x y = x - y

            The distance function is induced by the norm.

            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
              theorem SeminormedGroup.dist_eq {E : Type u_9} [self : SeminormedGroup E] (x : E) (y : E) :
              dist x y = x / y

              The distance function is induced by the norm.

              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
                theorem NormedAddGroup.dist_eq {E : Type u_9} [self : NormedAddGroup E] (x : E) (y : E) :
                dist x y = x - y

                The distance function is induced by the norm.

                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
                  theorem NormedGroup.dist_eq {E : Type u_9} [self : NormedGroup E] (x : E) (y : E) :
                  dist x y = x / y

                  The distance function is induced by the norm.

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

                  Instances
                    theorem SeminormedAddCommGroup.dist_eq {E : Type u_9} [self : SeminormedAddCommGroup E] (x : E) (y : E) :
                    dist x y = x - y

                    The distance function is induced by the norm.

                    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
                      theorem SeminormedCommGroup.dist_eq {E : Type u_9} [self : SeminormedCommGroup E] (x : E) (y : E) :
                      dist x y = x / y

                      The distance function is induced by the norm.

                      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
                        theorem NormedAddCommGroup.dist_eq {E : Type u_9} [self : NormedAddCommGroup E] (x : E) (y : E) :
                        dist x y = x - y

                        The distance function is induced by the norm.

                        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
                          theorem NormedCommGroup.dist_eq {E : Type u_9} [self : NormedCommGroup E] (x : E) (y : E) :
                          dist x y = x / y

                          The distance function is induced by the norm.

                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[instance 100]
                          Equations
                          @[reducible, inline]
                          abbrev 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
                            @[reducible, inline]
                            abbrev 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
                              @[reducible, inline]
                              abbrev 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, inline]
                                abbrev 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
                                  @[reducible, inline]
                                  abbrev 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, inline]
                                    abbrev 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, inline]
                                      abbrev 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
                                        @[reducible, inline]
                                        abbrev 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, inline]
                                          abbrev 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
                                            @[reducible, inline]
                                            abbrev 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, inline]
                                              abbrev 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
                                                @[reducible, inline]
                                                abbrev 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, inline]
                                                  abbrev 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, inline]
                                                    abbrev 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, inline]
                                                      abbrev 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, inline]
                                                        abbrev 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, inline]
                                                          abbrev NormedAddCommGroup.ofAddDist {E : Type u_6} [Norm E] [AddCommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

                                                          Construct a normed group from a translation-invariant pseudodistance.

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev 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, inline]
                                                              abbrev 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
                                                                @[reducible, inline]
                                                                abbrev 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
                                                                  @[reducible, inline]

                                                                  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, inline]

                                                                    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, inline]

                                                                      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, inline]

                                                                        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, inline]

                                                                          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, inline]
                                                                            abbrev GroupNorm.toNormedGroup {E : Type u_6} [Group E] (f : GroupNorm E) :

                                                                            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, inline]

                                                                              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, inline]

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

                                                                                  theorem DiscreteTopology.of_forall_le_norm {E : Type u_6} [SeminormedAddGroup E] {r : } (hpos : 0 < r) (hr : ∀ (x : E), x 0r x) :
                                                                                  theorem DiscreteTopology.of_forall_le_norm' {E : Type u_6} [SeminormedGroup E] {r : } (hpos : 0 < r) (hr : ∀ (x : E), x 1r x) :
                                                                                  @[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 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 : α) :
                                                                                  dist (s.indicator f x) (t.indicator f x) = (symmDiff s t).indicator f x
                                                                                  theorem dist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                  dist (s.mulIndicator f x) (t.mulIndicator f x) = (symmDiff s t).mulIndicator f x
                                                                                  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₂

                                                                                  Triangle inequality for the norm.

                                                                                  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₂

                                                                                  Triangle inequality for the norm.

                                                                                  theorem norm_add₃_le {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {c : E} :

                                                                                  Triangle inequality for the norm.

                                                                                  theorem norm_mul₃_le' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {c : E} :

                                                                                  Triangle inequality for the norm.

                                                                                  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) :
                                                                                      @[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.nhds_basis_norm_lt {E : Type u_6} [SeminormedAddGroup E] (x : E) :
                                                                                          (nhds x).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y - x < ε}
                                                                                          theorem NormedCommGroup.nhds_basis_norm_lt {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                          (nhds x).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y / x < ε}
                                                                                          theorem NormedAddCommGroup.nhds_zero_basis_norm_lt {E : Type u_6} [SeminormedAddGroup E] :
                                                                                          (nhds 0).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y < ε}
                                                                                          theorem NormedCommGroup.nhds_one_basis_norm_lt {E : Type u_6} [SeminormedGroup E] :
                                                                                          (nhds 1).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {y : E | y < ε}
                                                                                          theorem NormedAddCommGroup.uniformity_basis_dist {E : Type u_6} [SeminormedAddGroup E] :
                                                                                          (uniformity E).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {p : E × E | p.1 - p.2 < ε}
                                                                                          theorem NormedCommGroup.uniformity_basis_dist {E : Type u_6} [SeminormedGroup E] :
                                                                                          (uniformity E).HasBasis (fun (ε : ) => 0 < ε) fun (ε : ) => {p : E × E | p.1 / p.2 < ε}
                                                                                          @[instance 100]
                                                                                          Equations
                                                                                          • SeminormedAddGroup.toNNNorm = { nnnorm := fun (a : E) => a, }
                                                                                          @[instance 100]
                                                                                          Equations
                                                                                          • SeminormedGroup.toNNNorm = { nnnorm := fun (a : E) => a, }
                                                                                          @[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 norm_toNNReal {E : Type u_6} [SeminormedAddGroup E] {a : E} :
                                                                                          a.toNNReal = a‖₊
                                                                                          theorem norm_toNNReal' {E : Type u_6} [SeminormedGroup E] {a : E} :
                                                                                          a.toNNReal = a‖₊
                                                                                          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 nndist_zero_right {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                          @[simp]
                                                                                          theorem nndist_one_right {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                          @[simp]
                                                                                          theorem edist_zero_right {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                          edist a 0 = a‖₊
                                                                                          @[simp]
                                                                                          theorem edist_one_right {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                          edist a 1 = a‖₊
                                                                                          @[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) :
                                                                                          @[simp]
                                                                                          theorem nndist_zero_left {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                          @[simp]
                                                                                          theorem nndist_one_left {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                          @[simp]
                                                                                          theorem edist_zero_left {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                          edist 0 a = a‖₊
                                                                                          @[simp]
                                                                                          theorem edist_one_left {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                          edist 1 a = a‖₊
                                                                                          theorem nndist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                          nndist (s.indicator f x) (t.indicator f x) = (symmDiff s t).indicator f x‖₊
                                                                                          theorem nndist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                          nndist (s.mulIndicator f x) (t.mulIndicator f x) = (symmDiff s t).mulIndicator f 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 toReal_coe_nnnorm {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                          (↑a‖₊).toReal = a

                                                                                          The non negative norm seen as an ENNReal and then as a Real is equal to the norm.

                                                                                          theorem toReal_coe_nnnorm' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                          (↑a‖₊).toReal = a

                                                                                          The non negative norm seen as an ENNReal and then as a Real is equal to the norm.

                                                                                          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 : α) :
                                                                                          edist (s.indicator f x) (t.indicator f x) = (symmDiff s t).indicator f x‖₊
                                                                                          theorem edist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                          edist (s.mulIndicator f x) (t.mulIndicator f x) = (symmDiff s t).mulIndicator f x‖₊
                                                                                          theorem mem_emetric_ball_one_iff {E : Type u_6} [SeminormedGroup E] {a : E} {r : ENNReal} :
                                                                                          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.Pseudo.Defs 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)

                                                                                          See tendsto_norm_zero for a version with pointed neighborhoods.

                                                                                          theorem tendsto_norm_one {E : Type u_6} [SeminormedGroup E] :
                                                                                          Filter.Tendsto (fun (a : E) => a) (nhds 1) (nhds 0)

                                                                                          See tendsto_norm_one for a version with pointed neighborhoods.

                                                                                          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 Inseparable.norm_eq_norm {E : Type u_6} [SeminormedAddGroup E] {u : E} {v : E} (h : Inseparable u v) :
                                                                                          theorem Inseparable.norm_eq_norm' {E : Type u_6} [SeminormedGroup E] {u : E} {v : E} (h : Inseparable u v) :
                                                                                          theorem Inseparable.nnnorm_eq_nnnorm' {E : Type u_6} [SeminormedGroup E] {u : E} {v : E} (h : Inseparable u v) :
                                                                                          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.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 < εbs, a - b < ε
                                                                                          theorem SeminormedCommGroup.mem_closure_iff {E : Type u_6} [SeminormedGroup E] {s : Set E} {a : E} :
                                                                                          a closure s ∀ (ε : ), 0 < εbs, 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
                                                                                          @[reducible, inline]
                                                                                          abbrev 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, inline]
                                                                                            abbrev 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, inline]
                                                                                              abbrev 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
                                                                                                @[reducible, inline]
                                                                                                abbrev 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, inline]
                                                                                                  abbrev 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, inline]
                                                                                                    abbrev 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
                                                                                                      @[reducible, inline]
                                                                                                      abbrev 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, inline]
                                                                                                        abbrev 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) :
                                                                                                          theorem norm_multiset_sum_le {E : Type u_9} [SeminormedAddCommGroup E] (m : Multiset E) :
                                                                                                          m.sum (Multiset.map (fun (x : E) => x) m).sum
                                                                                                          theorem norm_multiset_prod_le {E : Type u_6} [SeminormedCommGroup E] (m : Multiset E) :
                                                                                                          m.prod (Multiset.map (fun (x : E) => x) m).sum
                                                                                                          theorem norm_sum_le {ι : Type u_9} {E : Type u_10} [SeminormedAddCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                          is, f i is, f i
                                                                                                          theorem norm_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                          is, f i is, 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) :
                                                                                                          bs, f b bs, 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) :
                                                                                                          bs, f b bs, 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 (∑ bs, f b) (∑ bs, a b) bs, 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 (∏ bs, f b) (∏ bs, a b) bs, d b
                                                                                                          theorem dist_sum_sum_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) (f : ιE) (a : ιE) :
                                                                                                          dist (∑ bs, f b) (∑ bs, a b) bs, 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 (∏ bs, f b) (∏ bs, a b) bs, 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 : ) => iFinset.range (n + 1), 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 : ) => iFinset.range (n + 1), 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 j.range) {f : } (b_pos : ∀ (n : ), 0 < f n) :
                                                                                                          ∃ (a : E), Filter.Tendsto (fun (n : ) => iFinset.range (n + 1), 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 j.range) {f : } (b_pos : ∀ (n : ), 0 < f n) :
                                                                                                          ∃ (a : E), Filter.Tendsto (fun (n : ) => iFinset.range (n + 1), j (a i)) Filter.atTop (nhds b) j (a 0) / b < f 0 ∀ (n : ), 0 < nj (a n) < f n
                                                                                                          theorem nnnorm_multiset_sum_le {E : Type u_6} [SeminormedAddCommGroup E] (m : Multiset E) :
                                                                                                          m.sum‖₊ (Multiset.map (fun (x : E) => x‖₊) m).sum
                                                                                                          theorem nnnorm_multiset_prod_le {E : Type u_6} [SeminormedCommGroup E] (m : Multiset E) :
                                                                                                          m.prod‖₊ (Multiset.map (fun (x : E) => x‖₊) m).sum
                                                                                                          theorem nnnorm_sum_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                          as, f a‖₊ as, f a‖₊
                                                                                                          theorem nnnorm_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ιE) :
                                                                                                          as, f a‖₊ as, 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) :
                                                                                                          bs, f b‖₊ bs, 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) :
                                                                                                          bs, f b‖₊ bs, 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) :
                                                                                                          @[simp]
                                                                                                          theorem Real.norm_natCast (n : ) :
                                                                                                          n = n
                                                                                                          @[simp]
                                                                                                          theorem Real.nnnorm_natCast (n : ) :
                                                                                                          n‖₊ = n
                                                                                                          @[deprecated Real.norm_natCast]
                                                                                                          theorem Real.norm_coe_nat (n : ) :
                                                                                                          n = n

                                                                                                          Alias of Real.norm_natCast.

                                                                                                          @[deprecated Real.nnnorm_natCast]
                                                                                                          theorem Real.nnnorm_coe_nat (n : ) :
                                                                                                          n‖₊ = n

                                                                                                          Alias of Real.nnnorm_natCast.

                                                                                                          @[simp]
                                                                                                          theorem Real.norm_ofNat (n : ) [n.AtLeastTwo] :
                                                                                                          @[simp]
                                                                                                          theorem Real.nnnorm_ofNat (n : ) [n.AtLeastTwo] :
                                                                                                          @[simp]
                                                                                                          theorem Real.norm_nnratCast (q : ℚ≥0) :
                                                                                                          q = q
                                                                                                          @[simp]
                                                                                                          theorem Real.nnnorm_nnratCast (q : ℚ≥0) :
                                                                                                          q‖₊ = q
                                                                                                          theorem Real.nnnorm_of_nonneg {r : } (hr : 0 r) :
                                                                                                          r‖₊ = r, hr
                                                                                                          @[simp]
                                                                                                          theorem Real.toNNReal_eq_nnnorm_of_nonneg {r : } (hr : 0 r) :
                                                                                                          r.toNNReal = r‖₊
                                                                                                          Equations
                                                                                                          @[simp]
                                                                                                          @[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
                                                                                                          theorem eq_zero_or_norm_pos {E : Type u_6} [NormedAddGroup E] (a : E) :
                                                                                                          a = 0 0 < a
                                                                                                          theorem eq_one_or_norm_pos {E : Type u_6} [NormedGroup E] (a : E) :
                                                                                                          a = 1 0 < a
                                                                                                          theorem eq_zero_or_nnnorm_pos {E : Type u_6} [NormedAddGroup E] (a : E) :
                                                                                                          a = 0 0 < a‖₊
                                                                                                          theorem eq_one_or_nnnorm_pos {E : Type u_6} [NormedGroup E] (a : E) :
                                                                                                          a = 1 0 < a‖₊
                                                                                                          @[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} :

                                                                                                          See tendsto_norm_zero for a version with full neighborhoods.

                                                                                                          See tendsto_norm_one for a version with full neighborhoods.

                                                                                                          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))

                                                                                                          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.

                                                                                                              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
                                                                                                              instance Subgroup.normedGroup {E : Type u_6} [NormedGroup E] {s : Subgroup E} :
                                                                                                              Equations
                                                                                                              Equations
                                                                                                              Equations

                                                                                                              Subgroup classes of normed groups #

                                                                                                              @[instance 75]

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

                                                                                                              Equations
                                                                                                              @[instance 75]
                                                                                                              instance SubgroupClass.seminormedGroup {E : Type u_6} [SeminormedGroup E] {S : Type u_9} [SetLike S E] [SubgroupClass S E] (s : S) :

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

                                                                                                              Equations
                                                                                                              @[simp]
                                                                                                              theorem AddSubgroupClass.coe_norm {E : Type u_6} [SeminormedAddGroup E] {S : Type u_9} [SetLike S E] [AddSubgroupClass S E] (s : S) (x : s) :

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

                                                                                                              @[simp]
                                                                                                              theorem SubgroupClass.coe_norm {E : Type u_6} [SeminormedGroup E] {S : Type u_9} [SetLike S E] [SubgroupClass S E] (s : S) (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.

                                                                                                              @[instance 75]
                                                                                                              instance AddSubgroupClass.normedAddGroup {E : Type u_6} [NormedAddGroup E] {S : Type u_9} [SetLike S E] [AddSubgroupClass S E] (s : S) :
                                                                                                              Equations
                                                                                                              @[instance 75]
                                                                                                              instance SubgroupClass.normedGroup {E : Type u_6} [NormedGroup E] {S : Type u_9} [SetLike S E] [SubgroupClass S E] (s : S) :
                                                                                                              Equations
                                                                                                              @[instance 75]
                                                                                                              instance SubgroupClass.normedCommGroup {E : Type u_6} [NormedCommGroup E] {S : Type u_9} [SetLike S E] [SubgroupClass S E] (s : S) :
                                                                                                              Equations
                                                                                                              theorem tendsto_norm_atTop_atTop :
                                                                                                              Filter.Tendsto norm Filter.atTop Filter.atTop