Documentation

Mathlib.Analysis.Normed.Field.UnitBall

Algebraic structures on unit balls and spheres #

In this file we define algebraic structures (Semigroup, CommSemigroup, Monoid, CommMonoid, Group, CommGroup) on Metric.ball (0 : ๐•œ) 1, Metric.closedBall (0 : ๐•œ) 1, and Metric.sphere (0 : ๐•œ) 1. In each case we use the weakest possible typeclass assumption on ๐•œ, from NonUnitalSeminormedRing to NormedField.

def Subsemigroup.unitBall (๐•œ : Type u_2) [NonUnitalSeminormedRing ๐•œ] :
Subsemigroup ๐•œ

Unit ball in a non unital semi normed ring as a bundled Subsemigroup.

Equations
Instances For
    instance Metric.unitBall.semigroup {๐•œ : Type u_1} [NonUnitalSeminormedRing ๐•œ] :
    Semigroup โ†‘(Metric.ball 0 1)
    Equations
    instance Metric.unitBall.continuousMul {๐•œ : Type u_1} [NonUnitalSeminormedRing ๐•œ] :
    Equations
    • โ‹ฏ = โ‹ฏ
    instance Metric.unitBall.commSemigroup {๐•œ : Type u_1} [SeminormedCommRing ๐•œ] :
    Equations
    instance Metric.unitBall.hasDistribNeg {๐•œ : Type u_1} [NonUnitalSeminormedRing ๐•œ] :
    Equations
    @[simp]
    theorem coe_mul_unitBall {๐•œ : Type u_1} [NonUnitalSeminormedRing ๐•œ] (x : โ†‘(Metric.ball 0 1)) (y : โ†‘(Metric.ball 0 1)) :
    โ†‘(x * y) = โ†‘x * โ†‘y
    def Subsemigroup.unitClosedBall (๐•œ : Type u_2) [NonUnitalSeminormedRing ๐•œ] :
    Subsemigroup ๐•œ

    Closed unit ball in a non unital semi normed ring as a bundled Subsemigroup.

    Equations
    Instances For
      instance Metric.unitClosedBall.semigroup {๐•œ : Type u_1} [NonUnitalSeminormedRing ๐•œ] :
      Equations
      Equations
      Equations
      • โ‹ฏ = โ‹ฏ
      @[simp]
      theorem coe_mul_unitClosedBall {๐•œ : Type u_1} [NonUnitalSeminormedRing ๐•œ] (x : โ†‘(Metric.closedBall 0 1)) (y : โ†‘(Metric.closedBall 0 1)) :
      โ†‘(x * y) = โ†‘x * โ†‘y
      def Submonoid.unitClosedBall (๐•œ : Type u_2) [SeminormedRing ๐•œ] [NormOneClass ๐•œ] :
      Submonoid ๐•œ

      Closed unit ball in a semi normed ring as a bundled Submonoid.

      Equations
      Instances For
        instance Metric.unitClosedBall.monoid {๐•œ : Type u_1} [SeminormedRing ๐•œ] [NormOneClass ๐•œ] :
        Equations
        instance Metric.unitClosedBall.commMonoid {๐•œ : Type u_1} [SeminormedCommRing ๐•œ] [NormOneClass ๐•œ] :
        Equations
        @[simp]
        theorem coe_one_unitClosedBall {๐•œ : Type u_1} [SeminormedRing ๐•œ] [NormOneClass ๐•œ] :
        โ†‘1 = 1
        @[simp]
        theorem coe_pow_unitClosedBall {๐•œ : Type u_1} [SeminormedRing ๐•œ] [NormOneClass ๐•œ] (x : โ†‘(Metric.closedBall 0 1)) (n : โ„•) :
        โ†‘(x ^ n) = โ†‘x ^ n
        @[simp]
        theorem Submonoid.unitSphere_coe (๐•œ : Type u_2) [NormedDivisionRing ๐•œ] :
        โ†‘(Submonoid.unitSphere ๐•œ) = Metric.sphere 0 1
        def Submonoid.unitSphere (๐•œ : Type u_2) [NormedDivisionRing ๐•œ] :
        Submonoid ๐•œ

        Unit sphere in a normed division ring as a bundled Submonoid.

        Equations
        Instances For
          instance Metric.unitSphere.inv {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
          Inv โ†‘(Metric.sphere 0 1)
          Equations
          @[simp]
          theorem coe_inv_unitSphere {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] (x : โ†‘(Metric.sphere 0 1)) :
          โ†‘xโปยน = (โ†‘x)โปยน
          instance Metric.unitSphere.div {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
          Div โ†‘(Metric.sphere 0 1)
          Equations
          • Metric.unitSphere.div = { div := fun (x y : โ†‘(Metric.sphere 0 1)) => โŸจโ†‘x / โ†‘y, โ‹ฏโŸฉ }
          @[simp]
          theorem coe_div_unitSphere {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] (x : โ†‘(Metric.sphere 0 1)) (y : โ†‘(Metric.sphere 0 1)) :
          โ†‘(x / y) = โ†‘x / โ†‘y
          instance Metric.unitSphere.pow {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
          Equations
          • Metric.unitSphere.pow = { pow := fun (x : โ†‘(Metric.sphere 0 1)) (n : โ„ค) => โŸจโ†‘x ^ n, โ‹ฏโŸฉ }
          @[simp]
          theorem coe_zpow_unitSphere {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] (x : โ†‘(Metric.sphere 0 1)) (n : โ„ค) :
          โ†‘(x ^ n) = โ†‘x ^ n
          instance Metric.unitSphere.monoid {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
          Monoid โ†‘(Metric.sphere 0 1)
          Equations
          @[simp]
          theorem coe_one_unitSphere {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
          โ†‘1 = 1
          @[simp]
          theorem coe_mul_unitSphere {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] (x : โ†‘(Metric.sphere 0 1)) (y : โ†‘(Metric.sphere 0 1)) :
          โ†‘(x * y) = โ†‘x * โ†‘y
          @[simp]
          theorem coe_pow_unitSphere {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] (x : โ†‘(Metric.sphere 0 1)) (n : โ„•) :
          โ†‘(x ^ n) = โ†‘x ^ n
          def unitSphereToUnits (๐•œ : Type u_2) [NormedDivisionRing ๐•œ] :
          โ†‘(Metric.sphere 0 1) โ†’* ๐•œหฃ

          Monoid homomorphism from the unit sphere to the group of units.

          Equations
          Instances For
            @[simp]
            theorem unitSphereToUnits_apply_coe {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] (x : โ†‘(Metric.sphere 0 1)) :
            โ†‘((unitSphereToUnits ๐•œ) x) = โ†‘x
            theorem unitSphereToUnits_injective {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
            instance Metric.sphere.group {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
            Group โ†‘(Metric.sphere 0 1)
            Equations
            instance Metric.sphere.hasDistribNeg {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
            Equations
            instance Metric.sphere.topologicalGroup {๐•œ : Type u_1} [NormedDivisionRing ๐•œ] :
            Equations
            • โ‹ฏ = โ‹ฏ
            instance Metric.sphere.commGroup {๐•œ : Type u_1} [NormedField ๐•œ] :
            Equations