Documentation

Mathlib.Analysis.Normed.Order.Basic

Ordered normed spaces #

In this file, we define classes for fields and groups that are both normed and ordered. These are mostly useful to avoid diamonds during type class inference.

A NormedOrderedAddGroup is an additive group that is both a NormedAddCommGroup and an OrderedAddCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

Instances
    theorem NormedOrderedAddGroup.dist_eq {α : Type u_2} [self : NormedOrderedAddGroup α] (x : α) (y : α) :
    dist x y = x - y

    The distance function is induced by the norm.

    class NormedOrderedGroup (α : Type u_2) extends OrderedCommGroup , Norm , MetricSpace :
    Type u_2

    A NormedOrderedGroup is a group that is both a NormedCommGroup and an OrderedCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

    Instances
      theorem NormedOrderedGroup.dist_eq {α : Type u_2} [self : NormedOrderedGroup α] (x : α) (y : α) :
      dist x y = x / y

      The distance function is induced by the norm.

      A NormedLinearOrderedAddGroup is an additive group that is both a NormedAddCommGroup and a LinearOrderedAddCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

      Instances
        theorem NormedLinearOrderedAddGroup.dist_eq {α : Type u_2} [self : NormedLinearOrderedAddGroup α] (x : α) (y : α) :
        dist x y = x - y

        The distance function is induced by the norm.

        A NormedLinearOrderedGroup is a group that is both a NormedCommGroup and a LinearOrderedCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

        Instances
          theorem NormedLinearOrderedGroup.dist_eq {α : Type u_2} [self : NormedLinearOrderedGroup α] (x : α) (y : α) :
          dist x y = x / y

          The distance function is induced by the norm.

          A NormedLinearOrderedField is a field that is both a NormedField and a LinearOrderedField. This class is necessary to avoid diamonds.

          Instances
            theorem NormedLinearOrderedField.dist_eq {α : Type u_2} [self : NormedLinearOrderedField α] (x : α) (y : α) :
            dist x y = x - y

            The distance function is induced by the norm.

            theorem NormedLinearOrderedField.norm_mul' {α : Type u_2} [self : NormedLinearOrderedField α] (x : α) (y : α) :

            The norm is multiplicative.

            @[instance 100]
            Equations
            @[instance 100]
            Equations
            @[instance 100]
            Equations
            @[instance 100]
            Equations
            Equations
            theorem OrderDual.normedOrderedAddGroup.proof_1 {α : Type u_1} [NormedOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
            a b∀ (c : αᵒᵈ), c + a c + b
            Equations
            theorem OrderDual.normedLinearOrderedAddGroup.proof_2 {α : Type u_1} [NormedLinearOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
            min a b = if a b then a else b
            theorem OrderDual.normedLinearOrderedAddGroup.proof_3 {α : Type u_1} [NormedLinearOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
            max a b = if a b then b else a
            Equations
            Equations