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.

source
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
source
@[protected, instance]
def metric.ball.semigroup {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
semigroup โ†ฅ(metric.ball 0 1)
Equations
source
@[protected, instance]
def metric.ball.has_continuous_mul {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
has_continuous_mul โ†ฅ(metric.ball 0 1)
source
@[protected, instance]
def metric.ball.comm_semigroup {๐•œ : Type u_1} [semi_normed_comm_ring ๐•œ] :
comm_semigroup โ†ฅ(metric.ball 0 1)
Equations
source
@[protected, instance]
def metric.ball.has_distrib_neg {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
has_distrib_neg โ†ฅ(metric.ball 0 1)
Equations
source
@[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
source
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
source
@[protected, instance]
def metric.closed_ball.semigroup {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
semigroup โ†ฅ(metric.closed_ball 0 1)
Equations
source
@[protected, instance]
def metric.closed_ball.has_distrib_neg {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
has_distrib_neg โ†ฅ(metric.closed_ball 0 1)
Equations
source
@[protected, instance]
def metric.closed_ball.has_continuous_mul {๐•œ : Type u_1} [non_unital_semi_normed_ring ๐•œ] :
has_continuous_mul โ†ฅ(metric.closed_ball 0 1)
source
@[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
source
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
source
@[protected, instance]
def metric.closed_ball.monoid {๐•œ : Type u_1} [semi_normed_ring ๐•œ] [norm_one_class ๐•œ] :
monoid โ†ฅ(metric.closed_ball 0 1)
Equations
source
@[protected, instance]
def metric.closed_ball.comm_monoid {๐•œ : Type u_1} [semi_normed_comm_ring ๐•œ] [norm_one_class ๐•œ] :
comm_monoid โ†ฅ(metric.closed_ball 0 1)
Equations
source
@[simp, norm_cast]
theorem coe_one_unit_closed_ball {๐•œ : Type u_1} [semi_normed_ring ๐•œ] [norm_one_class ๐•œ] :
โ†‘1 = 1
source
@[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
source
def submonoid.unit_sphere (๐•œ : Type u_1) [normed_division_ring ๐•œ] :
submonoid ๐•œ

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

Equations
source
@[protected, instance]
def metric.sphere.has_inv {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
has_inv โ†ฅ(metric.sphere 0 1)
Equations
source
@[simp, norm_cast]
theorem coe_inv_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x : โ†ฅ(metric.sphere 0 1)) :
โ†‘xโปยน = (โ†‘x)โปยน
source
@[protected, instance]
def metric.sphere.has_div {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
has_div โ†ฅ(metric.sphere 0 1)
Equations
source
@[simp, norm_cast]
theorem coe_div_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x y : โ†ฅ(metric.sphere 0 1)) :
โ†‘(x / y) = โ†‘x / โ†‘y
source
@[protected, instance]
def int.has_pow {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
has_pow โ†ฅ(metric.sphere 0 1) โ„ค
Equations
source
@[simp, norm_cast]
theorem coe_zpow_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x : โ†ฅ(metric.sphere 0 1)) (n : โ„ค) :
โ†‘(x ^ n) = โ†‘x ^ n
source
@[protected, instance]
def metric.sphere.monoid {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
monoid โ†ฅ(metric.sphere 0 1)
Equations
source
@[simp, norm_cast]
theorem coe_one_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
โ†‘1 = 1
source
@[simp, norm_cast]
theorem coe_mul_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x y : โ†ฅ(metric.sphere 0 1)) :
โ†‘(x * y) = โ†‘x * โ†‘y
source
@[simp, norm_cast]
theorem coe_pow_unit_sphere {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x : โ†ฅ(metric.sphere 0 1)) (n : โ„•) :
โ†‘(x ^ n) = โ†‘x ^ n
source
def unit_sphere_to_units (๐•œ : Type u_1) [normed_division_ring ๐•œ] :
โ†ฅ(metric.sphere 0 1) โ†’* ๐•œหฃ

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

Equations
source
@[simp]
theorem unit_sphere_to_units_apply_coe {๐•œ : Type u_1} [normed_division_ring ๐•œ] (x : โ†ฅ(metric.sphere 0 1)) :
โ†‘(โ‡‘(unit_sphere_to_units ๐•œ) x) = โ†‘x
source
theorem unit_sphere_to_units_injective {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
function.injective โ‡‘(unit_sphere_to_units ๐•œ)
source
@[protected, instance]
def metric.sphere.group {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
group โ†ฅ(metric.sphere 0 1)
Equations
source
@[protected, instance]
def metric.sphere.has_distrib_neg {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
has_distrib_neg โ†ฅ(metric.sphere 0 1)
Equations
source
@[protected, instance]
def metric.sphere.topological_group {๐•œ : Type u_1} [normed_division_ring ๐•œ] :
topological_group โ†ฅ(metric.sphere 0 1)
source
@[protected, instance]
def metric.sphere.comm_group {๐•œ : Type u_1} [normed_field ๐•œ] :
comm_group โ†ฅ(metric.sphere 0 1)
Equations