mathlib documentation

analysis.normed.field.unit_ball

Algebraic structures on unit balls and spheres #

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.

def subsemigroup.unit_ball (๐•œ : Type u_1) [non_unital_semi_normed_ring ๐•œ] :
subsemigroup ๐•œ

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

Equations
@[protected, instance]
def metric.ball.semigroup {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
Equations
@[protected, instance]
@[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)) :
def subsemigroup.unit_closed_ball (๐•œ : Type u_1) [non_unital_semi_normed_ring ๐•œ] :
subsemigroup ๐•œ

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

Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp, norm_cast]
theorem coe_mul_unit_closed_ball {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] (x y : โ†ฅ(metric.closed_ball 0 1)) :
def submonoid.unit_closed_ball (๐•œ : Type u_1) [semi_normed_ring ๐•œ] [norm_one_class ๐•œ] :
submonoid ๐•œ

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

Equations
@[protected, instance]
def metric.closed_ball.monoid {๐•œ : Type u_1} [semi_normed_ring ๐•œ] [norm_one_class ๐•œ] :
Equations
@[simp, norm_cast]
theorem coe_one_unit_closed_ball {๐•œ : Type u_1} [semi_normed_ring ๐•œ] [norm_one_class ๐•œ] :
@[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 ๐•œ] :
submonoid ๐•œ

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

Equations
@[protected, instance]
def metric.sphere.has_inv {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
Equations
@[simp, norm_cast]
theorem coe_inv_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x : โ†ฅ(metric.sphere 0 1)) :
@[protected, instance]
def metric.sphere.has_div {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
Equations
@[simp, norm_cast]
theorem coe_div_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x y : โ†ฅ(metric.sphere 0 1)) :
@[protected, instance]
def int.has_pow {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
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
@[protected, instance]
def metric.sphere.monoid {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
Equations
@[simp, norm_cast]
theorem coe_one_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
@[simp, norm_cast]
theorem coe_mul_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x y : โ†ฅ(metric.sphere 0 1)) :
@[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]
theorem unit_sphere_to_units_apply_coe {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x : โ†ฅ(metric.sphere 0 1)) :
@[protected, instance]
def metric.sphere.group {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
Equations
@[protected, instance]
Equations
@[protected, instance]