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.

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
  • norm : E

    the -valued norm function.

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.

Instances
    class NNNorm (E : Type u_9) :
    Type u_9
    • nnnorm : ENNReal

      the ℝ≥0-valued norm function.

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

    Instances

      the -valued norm function.

      Instances For

        the ℝ≥0-valued norm function.

        Instances For
          class SeminormedAddGroup (E : Type u_9) extends Norm , AddGroup , PseudoMetricSpace :
          Type u_9

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

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

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

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

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

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

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

                Instances

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

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

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

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

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

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

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

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

                          Construct a NormedAddGroup from a SeminormedAddGroup satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedAddGroup instance as a special case of a more general SeminormedAddGroup instance.

                          Instances For
                            theorem NormedAddGroup.ofSeparation.proof_1 {E : Type u_1} [SeminormedAddGroup E] (h : ∀ (x : E), x = 0x = 0) :
                            ∀ {x y : E}, dist x y = 0x = y
                            @[reducible]
                            def NormedGroup.ofSeparation {E : Type u_6} [SeminormedGroup E] (h : ∀ (x : E), x = 0x = 1) :

                            Construct a NormedGroup from a SeminormedGroup satisfying ∀ x, ‖x‖ = 0 → x = 1. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedGroup instance as a special case of a more general SeminormedGroup instance.

                            Instances For
                              @[reducible]
                              def NormedAddCommGroup.ofSeparation {E : Type u_6} [SeminormedAddCommGroup E] (h : ∀ (x : E), x = 0x = 0) :

                              Construct a NormedAddCommGroup from a SeminormedAddCommGroup satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedAddCommGroup instance as a special case of a more general SeminormedAddCommGroup instance.

                              Instances For
                                @[reducible]
                                def NormedCommGroup.ofSeparation {E : Type u_6} [SeminormedCommGroup E] (h : ∀ (x : E), x = 0x = 1) :

                                Construct a NormedCommGroup from a SeminormedCommGroup satisfying ∀ x, ‖x‖ = 0 → x = 1. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedCommGroup instance as a special case of a more general SeminormedCommGroup instance.

                                Instances For
                                  theorem SeminormedAddGroup.ofAddDist.proof_1 {E : Type u_1} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) (x : E) (y : E) :
                                  dist x y = x - y
                                  def SeminormedAddGroup.ofAddDist {E : Type u_6} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), x = dist x 0) (h₂ : ∀ (x y z : E), dist x y dist (x + z) (y + z)) :

                                  Construct a seminormed group from a translation-invariant distance.

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

                                    Construct a seminormed group from a multiplication-invariant distance.

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

                                      Construct a seminormed group from a translation-invariant pseudodistance.

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

                                        Construct a seminormed group from a multiplication-invariant pseudodistance.

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

                                          Construct a seminormed group from a translation-invariant pseudodistance.

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

                                            Construct a seminormed group from a multiplication-invariant pseudodistance.

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

                                              Construct a seminormed group from a translation-invariant pseudodistance.

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

                                                Construct a seminormed group from a multiplication-invariant pseudodistance.

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

                                                  Construct a normed group from a translation-invariant distance.

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

                                                    Construct a normed group from a multiplication-invariant distance.

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

                                                      Construct a normed group from a translation-invariant pseudodistance.

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

                                                        Construct a normed group from a multiplication-invariant pseudodistance.

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

                                                          Construct a normed group from a translation-invariant pseudodistance.

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

                                                            Construct a normed group from a multiplication-invariant pseudodistance.

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

                                                              Construct a normed group from a translation-invariant pseudodistance.

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

                                                                Construct a normed group from a multiplication-invariant pseudodistance.

                                                                Instances For
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_4 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                  0 f (x - y)
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) :
                                                                  f (x - x) = 0
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_3 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (a : E) (b : E) (c : E) :
                                                                  f (a - c) f (a - b) + f (b - c)
                                                                  theorem AddGroupSeminorm.toSeminormedAddGroup.proof_5 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                  { val := f (x - y), property := (_ : 0 f (x - y)) } = ENNReal.ofReal { val := f (x - y), property := (_ : 0 f (x - y)) }

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

                                                                  Instances For
                                                                    theorem AddGroupSeminorm.toSeminormedAddGroup.proof_8 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                    dist x y = dist x y
                                                                    theorem AddGroupSeminorm.toSeminormedAddGroup.proof_2 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) :
                                                                    f (x - y) = f (y - x)

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

                                                                    Instances For

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

                                                                      Instances For
                                                                        theorem AddGroupSeminorm.toSeminormedAddCommGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                                        a + b = b + a

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

                                                                        Instances For

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

                                                                          Instances For
                                                                            theorem AddGroupNorm.toNormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) :
                                                                            ∀ {x y : E}, dist x y = 0x = y

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

                                                                            Instances For
                                                                              theorem AddGroupNorm.toNormedAddCommGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) :
                                                                              a + b = b + a

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

                                                                              Instances For

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

                                                                                Instances For
                                                                                  theorem dist_eq_norm_sub {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = a - b
                                                                                  theorem dist_eq_norm_div {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist a b = a / b
                                                                                  theorem dist_eq_norm_sub' {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = b - a
                                                                                  theorem dist_eq_norm_div' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist a b = b / a
                                                                                  theorem dist_eq_norm {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist a b = a - b

                                                                                  Alias of dist_eq_norm_sub.

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

                                                                                  Alias of dist_eq_norm_sub'.

                                                                                  @[simp]
                                                                                  theorem dist_zero_right {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem dist_one_right {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem dist_zero_left {E : Type u_6} [SeminormedAddGroup E] :
                                                                                  dist 0 = norm
                                                                                  @[simp]
                                                                                  theorem dist_one_left {E : Type u_6} [SeminormedGroup E] :
                                                                                  dist 1 = norm
                                                                                  theorem Isometry.norm_map_of_map_zero {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :
                                                                                  theorem Isometry.norm_map_of_map_one {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
                                                                                  theorem norm_sub_rev {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  a - b = b - a
                                                                                  theorem norm_div_rev {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  a / b = b / a
                                                                                  @[simp]
                                                                                  theorem norm_neg {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem norm_inv' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                  theorem dist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                  theorem dist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                  @[simp]
                                                                                  theorem dist_add_self_right {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist b (a + b) = a
                                                                                  @[simp]
                                                                                  theorem dist_mul_self_right {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist b (a * b) = a
                                                                                  @[simp]
                                                                                  theorem dist_add_self_left {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                  dist (a + b) b = a
                                                                                  @[simp]
                                                                                  theorem dist_mul_self_left {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                  dist (a * b) b = a
                                                                                  @[simp]
                                                                                  theorem dist_sub_eq_dist_add_left {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist (a - b) c = dist a (c + b)
                                                                                  @[simp]
                                                                                  theorem dist_div_eq_dist_mul_left {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist (a / b) c = dist a (c * b)
                                                                                  @[simp]
                                                                                  theorem dist_sub_eq_dist_add_right {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist a (b - c) = dist (a + c) b
                                                                                  @[simp]
                                                                                  theorem dist_div_eq_dist_mul_right {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  dist a (b / c) = dist (a * c) b
                                                                                  theorem Filter.tendsto_neg_cobounded {E : Type u_6} [SeminormedAddGroup E] :
                                                                                  Filter.Tendsto Neg.neg (Filter.comap norm Filter.atTop) (Filter.comap norm Filter.atTop)

                                                                                  In a (semi)normed group, negation x ↦ -x tends to infinity at infinity. TODO: use Bornology.cobounded instead of Filter.comap Norm.norm Filter.atTop.

                                                                                  theorem Filter.tendsto_inv_cobounded {E : Type u_6} [SeminormedGroup E] :
                                                                                  Filter.Tendsto Inv.inv (Filter.comap norm Filter.atTop) (Filter.comap norm Filter.atTop)

                                                                                  In a (semi)normed group, inversion x ↦ x⁻¹ tends to infinity at infinity. TODO: use Bornology.cobounded instead of Filter.comap Norm.norm Filter.atTop.

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

                                                                                  Triangle inequality for the norm.

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

                                                                                  Triangle inequality for the norm.

                                                                                  theorem norm_add_le_of_le {E : Type u_6} [SeminormedAddGroup E] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
                                                                                  a₁ + a₂ r₁ + r₂
                                                                                  theorem norm_mul_le_of_le {E : Type u_6} [SeminormedGroup E] {a₁ : E} {a₂ : E} {r₁ : } {r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
                                                                                  a₁ * a₂ r₁ + r₂
                                                                                  theorem norm_add₃_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) :
                                                                                  theorem norm_mul₃_le {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) :
                                                                                  @[simp]
                                                                                  theorem norm_nonneg {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                  @[simp]
                                                                                  theorem norm_nonneg' {E : Type u_6} [SeminormedGroup E] (a : 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 | x - y < ε}
                                                                                      theorem ball_eq' {E : Type u_6} [SeminormedGroup E] (y : E) (ε : ) :
                                                                                      Metric.ball y ε = {x | x / y < ε}
                                                                                      theorem ball_zero_eq {E : Type u_6} [SeminormedAddGroup E] (r : ) :
                                                                                      Metric.ball 0 r = {x | x < r}
                                                                                      theorem ball_one_eq {E : Type u_6} [SeminormedGroup E] (r : ) :
                                                                                      Metric.ball 1 r = {x | x < r}
                                                                                      theorem mem_ball_iff_norm {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_iff_norm'' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_iff_norm' {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_iff_norm''' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_ball_zero_iff {E : Type u_6} [SeminormedAddGroup E] {a : E} {r : } :
                                                                                      theorem mem_ball_one_iff {E : Type u_6} [SeminormedGroup E] {a : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm'' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm' {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem mem_closedBall_iff_norm''' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      theorem norm_le_of_mem_closedBall {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } (h : b Metric.closedBall a r) :
                                                                                      theorem norm_le_of_mem_closedBall' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } (h : b Metric.closedBall a r) :
                                                                                      theorem norm_le_norm_add_const_of_dist_le {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } :
                                                                                      dist a b ra b + r
                                                                                      theorem norm_le_norm_add_const_of_dist_le' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } :
                                                                                      dist a b ra b + r
                                                                                      theorem norm_lt_of_mem_ball {E : Type u_6} [SeminormedAddGroup E] {a : E} {b : E} {r : } (h : b Metric.ball a r) :
                                                                                      theorem norm_lt_of_mem_ball' {E : Type u_6} [SeminormedGroup E] {a : E} {b : E} {r : } (h : b Metric.ball a r) :
                                                                                      theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_6} [SeminormedAddGroup E] (u : E) (v : E) (w : E) :
                                                                                      theorem norm_div_sub_norm_div_le_norm_div {E : Type u_6} [SeminormedGroup E] (u : E) (v : E) (w : E) :
                                                                                      theorem isBounded_iff_forall_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded s C, ∀ (x : E), x sx C
                                                                                      theorem isBounded_iff_forall_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded s C, ∀ (x : E), x sx C
                                                                                      theorem Bornology.IsBounded.exists_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} :
                                                                                      Bornology.IsBounded sC, ∀ (x : E), x sx C

                                                                                      Alias of the forward direction of isBounded_iff_forall_norm_le'.

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

                                                                                      Alias of the forward direction of isBounded_iff_forall_norm_le.

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

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

                                                                                        Instances For

                                                                                          The norm of a seminormed group as a group seminorm.

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

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

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

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

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

                                                                                            Alias of the forward direction of lipschitzOnWith_iff_norm_div_le.

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

                                                                                            Alias of the forward direction of lipschitzWith_iff_norm_div_le.

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

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

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

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

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

                                                                                            Alias of the reverse direction of MonoidHomClass.isometry_iff_norm.

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

                                                                                            Alias of nndist_eq_nnnorm_sub.

                                                                                            @[simp]
                                                                                            theorem nnnorm_zero {E : Type u_6} [SeminormedAddGroup E] :
                                                                                            @[simp]
                                                                                            theorem nnnorm_one' {E : Type u_6} [SeminormedGroup E] :
                                                                                            theorem ne_zero_of_nnnorm_ne_zero {E : Type u_6} [SeminormedAddGroup E] {a : E} :
                                                                                            a‖₊ 0a 0
                                                                                            theorem ne_one_of_nnnorm_ne_zero {E : Type u_6} [SeminormedGroup E] {a : E} :
                                                                                            a‖₊ 0a 1
                                                                                            theorem nnnorm_add_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                            theorem nnnorm_mul_le' {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                            @[simp]
                                                                                            theorem nnnorm_neg {E : Type u_6} [SeminormedAddGroup E] (a : E) :
                                                                                            @[simp]
                                                                                            theorem nnnorm_inv' {E : Type u_6} [SeminormedGroup E] (a : E) :
                                                                                            theorem nndist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                            theorem nndist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                            theorem nnnorm_sub_le {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                            theorem nnnorm_div_le {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                            theorem edist_eq_coe_nnnorm_sub {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) :
                                                                                            edist a b = a - b‖₊
                                                                                            theorem edist_eq_coe_nnnorm_div {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) :
                                                                                            edist a b = a / b‖₊
                                                                                            theorem edist_eq_coe_nnnorm {E : Type u_6} [SeminormedAddGroup E] (x : E) :
                                                                                            edist x 0 = x‖₊
                                                                                            theorem edist_eq_coe_nnnorm' {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                            edist x 1 = x‖₊
                                                                                            theorem edist_indicator {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                            theorem edist_mulIndicator {α : Type u_3} {E : Type u_6} [SeminormedGroup E] (s : Set α) (t : Set α) (f : αE) (x : α) :
                                                                                            theorem mem_emetric_ball_one_iff {E : Type u_6} [SeminormedGroup E] {a : E} {r : ENNReal} :
                                                                                            theorem AddMonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), f x‖₊ C * x‖₊) :
                                                                                            theorem MonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), f x‖₊ C * x‖₊) :
                                                                                            theorem AddMonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), x K * f x) :
                                                                                            theorem MonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), x K * f x) :
                                                                                            theorem LipschitzWith.norm_le_mul {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                            f x K * x
                                                                                            theorem LipschitzWith.norm_le_mul' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                            f x K * x
                                                                                            theorem LipschitzWith.nnorm_le_mul {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                            theorem LipschitzWith.nnorm_le_mul' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                            theorem AntilipschitzWith.le_mul_norm {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                            x K * f x
                                                                                            theorem AntilipschitzWith.le_mul_norm' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                            x K * f x
                                                                                            theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :
                                                                                            theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :
                                                                                            theorem ZeroHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
                                                                                            x K * f x
                                                                                            theorem OneHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
                                                                                            x K * f x
                                                                                            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 1. In this pair of lemmas (squeeze_zero_norm' and squeeze_zero_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_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. 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 => a - x) (nhds x) (nhds 0)
                                                                                            theorem tendsto_norm_div_self {E : Type u_6} [SeminormedGroup E] (x : E) :
                                                                                            Filter.Tendsto (fun a => a / x) (nhds x) (nhds 0)
                                                                                            theorem tendsto_norm {E : Type u_6} [SeminormedAddGroup E] {x : E} :
                                                                                            Filter.Tendsto (fun a => a) (nhds x) (nhds x)
                                                                                            theorem tendsto_norm' {E : Type u_6} [SeminormedGroup E] {x : E} :
                                                                                            Filter.Tendsto (fun a => a) (nhds x) (nhds x)
                                                                                            theorem tendsto_norm_zero {E : Type u_6} [SeminormedAddGroup E] :
                                                                                            Filter.Tendsto (fun a => a) (nhds 0) (nhds 0)
                                                                                            theorem tendsto_norm_one {E : Type u_6} [SeminormedGroup E] :
                                                                                            Filter.Tendsto (fun a => a) (nhds 1) (nhds 0)
                                                                                            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 | x = 0}
                                                                                            theorem closure_one_eq {E : Type u_6} [SeminormedGroup E] :
                                                                                            closure {1} = {x | x = 0}
                                                                                            theorem Filter.Tendsto.op_zero_isBoundedUnder_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : αE} {g : αF} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun x x_1 => x x_1) l (norm g)) (op : EFG) (h_op : A, ∀ (x : E) (y : F), op x y A * x * y) :
                                                                                            Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 0)

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

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

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

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

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

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

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

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

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

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

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

                                                                                            theorem SeminormedAddCommGroup.mem_closure_iff {E : Type u_6} [SeminormedAddGroup E] {s : Set E} {a : E} :
                                                                                            a closure s ∀ (ε : ), 0 < εb, b s a - b < ε
                                                                                            theorem SeminormedCommGroup.mem_closure_iff {E : Type u_6} [SeminormedGroup E] {s : Set E} {a : E} :
                                                                                            a closure s ∀ (ε : ), 0 < εb, b s a / b < ε
                                                                                            theorem norm_le_zero_iff' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} :
                                                                                            a 0 a = 0
                                                                                            theorem norm_le_zero_iff''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} :
                                                                                            a 0 a = 1
                                                                                            theorem norm_eq_zero' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} :
                                                                                            a = 0 a = 0
                                                                                            theorem norm_eq_zero''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} :
                                                                                            a = 0 a = 1
                                                                                            theorem norm_pos_iff' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} :
                                                                                            0 < a a 0
                                                                                            theorem norm_pos_iff''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} :
                                                                                            0 < a a 1
                                                                                            theorem SeminormedAddGroup.tendstoUniformlyOn_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [SeminormedAddGroup G] {f : ικG} {s : Set κ} {l : Filter ι} :
                                                                                            TendstoUniformlyOn f 0 l s ∀ (ε : ), ε > 0∀ᶠ (i : ι) in l, ∀ (x : κ), x sf 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, ∀ (x : κ), x sf 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.fst z - f n.snd 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.fst z / f n.snd 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.fst z - f n.snd 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.fst z / f n.snd z) 1 (l ×ˢ l) s
                                                                                            theorem SeminormedAddGroup.induced.proof_1 {𝓕 : Type u_3} (E : Type u_1) (F : Type u_2) [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (x : E) (y : E) :
                                                                                            dist x y = x - y
                                                                                            @[reducible]
                                                                                            def SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) :

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

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

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

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

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

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

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

                                                                                                  Instances For
                                                                                                    @[reducible]
                                                                                                    def NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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.

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

                                                                                                      An injective group homomorphism from a Group to a NormedGr