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.

source
class NormedOrderedAddGroup (α : Type u_2) extends OrderedAddCommGroup , Norm , MetricSpace , AddCommGroup , PartialOrder , AddGroup , AddCommMonoid , SubNegMonoid , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Preorder , LE , LT , PseudoMetricSpace , Dist :
Type u_2

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
    source
    theorem NormedOrderedAddGroup.dist_eq {α : Type u_2} [self : NormedOrderedAddGroup α] (x : α) (y : α) :
    dist x y = ‖x - y‖

    The distance function is induced by the norm.

    source
    class NormedOrderedGroup (α : Type u_2) extends OrderedCommGroup , Norm , MetricSpace , CommGroup , PartialOrder , Group , CommMonoid , DivInvMonoid , Monoid , Inv , Div , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Preorder , LE , LT , PseudoMetricSpace , Dist :
    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
      source
      theorem NormedOrderedGroup.dist_eq {α : Type u_2} [self : NormedOrderedGroup α] (x : α) (y : α) :
      dist x y = ‖x / y‖

      The distance function is induced by the norm.

      source
      class NormedLinearOrderedAddGroup (α : Type u_2) extends LinearOrderedAddCommGroup , Norm , MetricSpace , OrderedAddCommGroup , LinearOrder , AddCommGroup , PartialOrder , AddGroup , AddCommMonoid , SubNegMonoid , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT , PseudoMetricSpace , Dist :
      Type u_2

      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
        source
        theorem NormedLinearOrderedAddGroup.dist_eq {α : Type u_2} [self : NormedLinearOrderedAddGroup α] (x : α) (y : α) :
        dist x y = ‖x - y‖

        The distance function is induced by the norm.

        source
        class NormedLinearOrderedGroup (α : Type u_2) extends LinearOrderedCommGroup , Norm , MetricSpace , OrderedCommGroup , LinearOrder , CommGroup , PartialOrder , Group , CommMonoid , DivInvMonoid , Monoid , Inv , Div , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Min , Max , Ord , Preorder , LE , LT , PseudoMetricSpace , Dist :
        Type u_2

        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
          source
          theorem NormedLinearOrderedGroup.dist_eq {α : Type u_2} [self : NormedLinearOrderedGroup α] (x : α) (y : α) :
          dist x y = ‖x / y‖

          The distance function is induced by the norm.

          source
          class NormedLinearOrderedField (α : Type u_2) extends LinearOrderedField , Norm , MetricSpace , LinearOrderedCommRing , Field , LinearOrderedRing , CommRing , DivisionRing , CommMonoid , StrictOrderedRing , LinearOrder , Ring , OrderedAddCommGroup , DivInvMonoid , Nontrivial , NNRatCast , RatCast , Semiring , AddCommGroup , AddGroupWithOne , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , CommSemigroup , Inv , Div , MulOneClass , IntCast , AddMonoidWithOne , PartialOrder , AddGroup , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , CommMagma , Mul , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT , PseudoMetricSpace , Dist :
          Type u_2

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

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

            The distance function is induced by the norm.

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

            The norm is multiplicative.

            source
            @[instance 100]
            instance NormedOrderedGroup.toNormedCommGroup {α : Type u_1} [NormedOrderedGroup α] :
            NormedCommGroup α
            Equations
            source
            @[instance 100]
            instance NormedOrderedAddGroup.toNormedAddCommGroup {α : Type u_1} [NormedOrderedAddGroup α] :
            NormedAddCommGroup α
            Equations
            source
            @[instance 100]
            instance NormedLinearOrderedGroup.toNormedOrderedGroup {α : Type u_1} [NormedLinearOrderedGroup α] :
            NormedOrderedGroup α
            Equations
            source
            @[instance 100]
            instance NormedLinearOrderedAddGroup.toNormedOrderedAddGroup {α : Type u_1} [NormedLinearOrderedAddGroup α] :
            NormedOrderedAddGroup α
            Equations
            source
            @[instance 100]
            instance NormedLinearOrderedField.toNormedField (α : Type u_2) [NormedLinearOrderedField α] :
            NormedField α
            Equations
            source
            instance Rat.normedLinearOrderedField :
            NormedLinearOrderedField ℚ
            Equations
            source
            noncomputable instance Real.normedLinearOrderedField :
            NormedLinearOrderedField ℝ
            Equations
            source
            instance OrderDual.normedOrderedGroup {α : Type u_1} [NormedOrderedGroup α] :
            NormedOrderedGroup αᵒᵈ
            Equations
            source
            instance OrderDual.normedOrderedAddGroup {α : Type u_1} [NormedOrderedAddGroup α] :
            NormedOrderedAddGroup αᵒᵈ
            Equations
            source
            instance OrderDual.normedLinearOrderedGroup {α : Type u_1} [NormedLinearOrderedGroup α] :
            NormedLinearOrderedGroup αᵒᵈ
            Equations
            source
            instance OrderDual.normedLinearOrderedAddGroup {α : Type u_1} [NormedLinearOrderedAddGroup α] :
            NormedLinearOrderedAddGroup αᵒᵈ
            Equations
            source
            instance Additive.normedOrderedAddGroup {α : Type u_1} [NormedOrderedGroup α] :
            NormedOrderedAddGroup (Additive α)
            Equations
            source
            instance Multiplicative.normedOrderedGroup {α : Type u_1} [NormedOrderedAddGroup α] :
            NormedOrderedGroup (Multiplicative α)
            Equations
            source
            instance Additive.normedLinearOrderedAddGroup {α : Type u_1} [NormedLinearOrderedGroup α] :
            NormedLinearOrderedAddGroup (Additive α)
            Equations
            source
            instance Multiplicative.normedlinearOrderedGroup {α : Type u_1} [NormedLinearOrderedAddGroup α] :
            NormedLinearOrderedGroup (Multiplicative α)
            Equations