mathlib3 documentation

analysis.normed.field.unit_ball

Algebraic structures on unit balls and spheres #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define algebraic structures (semigroup, comm_semigroup, monoid, comm_monoid, group, comm_group) on metric.ball (0 : 𝕜) 1, metric.closed_ball (0 : 𝕜) 1, and metric.sphere (0 : 𝕜) 1. In each case we use the weakest possible typeclass assumption on 𝕜, from non_unital_semi_normed_ring to normed_field.

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

Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_mul_unit_ball {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] (x y : (metric.ball 0 1)) :
(x * y) = x * y

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

Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_mul_unit_closed_ball {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] (x y : (metric.closed_ball 0 1)) :
(x * y) = x * y

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

Equations
@[simp, norm_cast]
theorem coe_one_unit_closed_ball {𝕜 : Type u_1} [semi_normed_ring 𝕜] [norm_one_class 𝕜] :
1 = 1
@[simp, norm_cast]
theorem coe_pow_unit_closed_ball {𝕜 : Type u_1} [semi_normed_ring 𝕜] [norm_one_class 𝕜] (x : (metric.closed_ball 0 1)) (n : ) :
(x ^ n) = x ^ n
def submonoid.unit_sphere (𝕜 : Type u_1) [normed_division_ring 𝕜] :

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

Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_inv_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x : (metric.sphere 0 1)) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_div_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x y : (metric.sphere 0 1)) :
(x / y) = x / y
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_zpow_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x : (metric.sphere 0 1)) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem coe_one_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] :
1 = 1
@[simp, norm_cast]
theorem coe_mul_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x y : (metric.sphere 0 1)) :
(x * y) = x * y
@[simp, norm_cast]
theorem coe_pow_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x : (metric.sphere 0 1)) (n : ) :
(x ^ n) = x ^ n
def unit_sphere_to_units (𝕜 : Type u_1) [normed_division_ring 𝕜] :

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

Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]