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.

Algebraic structures on `Metric.ball 0 1` #

def Subsemigroup.unitBall (𝕜 : Type u_2) [NonUnitalSeminormedRing 𝕜] :

Subsemigroup 𝕜

Unit ball in a non-unital seminormed ring as a bundled Subsemigroup.

Equations

Instances For

instance Metric.unitBall.instSemigroup {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

Semigroup ↑(ball 0 1)

Equations

instance Metric.unitBall.instContinuousMul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

ContinuousMul ↑(ball 0 1)

instance Metric.unitBall.instCommSemigroup {𝕜 : Type u_1} [SeminormedCommRing 𝕜] :

CommSemigroup ↑(ball 0 1)

Equations

instance Metric.unitBall.instHasDistribNeg {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

HasDistribNeg ↑(ball 0 1)

Equations

@[simp]

theorem Metric.unitBall.coe_mul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] (x y : ↑(ball 0 1)) :

↑(x * y) = ↑x * ↑y

instance Metric.unitBall.instZero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :

Zero ↑(ball 0 1)

Equations

@[simp]

theorem Metric.unitBall.coe_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :

↑0 = 0

@[simp]

theorem Metric.unitBall.coe_eq_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] {a : ↑(ball 0 1)} :

↑a = 0 ↔ a = 0

instance Metric.unitBall.instSemigroupWithZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

SemigroupWithZero ↑(ball 0 1)

Equations

instance Metric.unitBall.instIsLeftCancelMulZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] [IsLeftCancelMulZero 𝕜] :

IsLeftCancelMulZero ↑(ball 0 1)

instance Metric.unitBall.instIsRightCancelMulZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] [IsRightCancelMulZero 𝕜] :

IsRightCancelMulZero ↑(ball 0 1)

instance Metric.unitBall.instIsCancelMulZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] [IsCancelMulZero 𝕜] :

IsCancelMulZero ↑(ball 0 1)

Algebraic instances for `Metric.closedBall 0 1` #

def Subsemigroup.unitClosedBall (𝕜 : Type u_2) [NonUnitalSeminormedRing 𝕜] :

Subsemigroup 𝕜

Closed unit ball in a non-unital seminormed ring as a bundled Subsemigroup.

Equations

Instances For

instance Metric.unitClosedBall.instSemigroup {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

Semigroup ↑(closedBall 0 1)

Equations

instance Metric.unitClosedBall.instHasDistribNeg {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

HasDistribNeg ↑(closedBall 0 1)

Equations

instance Metric.unitClosedBall.instContinuousMul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

ContinuousMul ↑(closedBall 0 1)

@[simp]

theorem Metric.unitClosedBall.coe_mul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] (x y : ↑(closedBall 0 1)) :

↑(x * y) = ↑x * ↑y

instance Metric.unitClosedBall.instZero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :

Zero ↑(closedBall 0 1)

Equations

@[simp]

theorem Metric.unitClosedBall.coe_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :

↑0 = 0

@[simp]

theorem Metric.unitClosedBall.coe_eq_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] {a : ↑(closedBall 0 1)} :

↑a = 0 ↔ a = 0

instance Metric.unitClosedBall.instSemigroupWithZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

SemigroupWithZero ↑(closedBall 0 1)

Equations

def Submonoid.unitClosedBall (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormOneClass 𝕜] :

Closed unit ball in a seminormed ring as a bundled Submonoid.

Equations

Instances For

instance Metric.unitClosedBall.instMonoid {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :

Monoid ↑(closedBall 0 1)

Equations

instance Metric.unitClosedBall.instCommMonoid {𝕜 : Type u_1} [SeminormedCommRing 𝕜] [NormOneClass 𝕜] :

CommMonoid ↑(closedBall 0 1)

Equations

@[simp]

theorem Metric.unitClosedBall.coe_one {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :

↑1 = 1

@[simp]

theorem Metric.unitClosedBall.coe_eq_one {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] {a : ↑(closedBall 0 1)} :

↑a = 1 ↔ a = 1

@[simp]

theorem Metric.unitClosedBall.coe_pow {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] (x : ↑(closedBall 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

instance Metric.unitClosedBall.instMonoidWithZero {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :

MonoidWithZero ↑(closedBall 0 1)

Equations

instance Metric.unitClosedBall.instIsCancelMulZero {𝕜 : Type u_1} [SeminormedRing 𝕜] [IsCancelMulZero 𝕜] [NormOneClass 𝕜] :

IsCancelMulZero ↑(closedBall 0 1)

Algebraic instances on the unit sphere #

def Submonoid.unitSphere (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

Unit sphere in a seminormed ring (with strictly multiplicative norm) as a bundled Submonoid.

Equations

Instances For

@[simp]

theorem Submonoid.coe_unitSphere (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

↑(unitSphere 𝕜) = Metric.sphere 0 1

instance Metric.unitSphere.instInv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Inv ↑(sphere 0 1)

Equations

@[simp]

theorem Metric.unitSphere.coe_inv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(sphere 0 1)) :

↑x⁻¹ = (↑x)⁻¹

instance Metric.unitSphere.instDiv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Div ↑(sphere 0 1)

Equations

@[simp]

theorem Metric.unitSphere.coe_div {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x y : ↑(sphere 0 1)) :

↑(x / y) = ↑x / ↑y

instance Metric.unitSphere.instZPow {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Pow ↑(sphere 0 1) ℤ

Equations

@[simp]

theorem Metric.unitSphere.coe_zpow {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(sphere 0 1)) (n : ℤ) :

↑(x ^ n) = ↑x ^ n

instance Metric.unitSphere.instMonoid {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

Monoid ↑(sphere 0 1)

Equations

instance Metric.unitSphere.instCommMonoid {𝕜 : Type u_1} [SeminormedCommRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

CommMonoid ↑(sphere 0 1)

Equations

@[simp]

theorem Metric.unitSphere.coe_one {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

↑1 = 1

@[simp]

theorem Metric.unitSphere.coe_mul {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x y : ↑(sphere 0 1)) :

↑(x * y) = ↑x * ↑y

@[simp]

theorem Metric.unitSphere.coe_pow {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x : ↑(sphere 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

def unitSphereToUnits (𝕜 : Type u_2) [NormedDivisionRing 𝕜] :

↑(Metric.sphere 0 1) →* 𝕜ˣ

Monoid homomorphism from the unit sphere in a normed division ring 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 𝕜] :

Function.Injective ⇑(unitSphereToUnits 𝕜)

instance Metric.unitSphere.instGroup {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Group ↑(sphere 0 1)

Equations

instance Metric.sphere.instHasDistribNeg {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

HasDistribNeg ↑(sphere 0 1)

Equations

instance Metric.sphere.instContinuousMul {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :

ContinuousMul ↑(sphere 0 1)

instance Metric.sphere.instIsTopologicalGroup {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

IsTopologicalGroup ↑(sphere 0 1)

instance Metric.sphere.instCommGroup {𝕜 : Type u_1} [NormedField 𝕜] :

CommGroup ↑(sphere 0 1)

Equations