UnitBall

📁 Source: Mathlib/Analysis/Normed/Field/UnitBall.lean

Statistics

Metric	Count
Definitions instCommGroup, instHasDistribNeg, instCommSemigroup, instHasDistribNeg, instSemigroup, instSemigroupWithZero, instZero, instCommMonoid, instHasDistribNeg, instMonoid, instMonoidWithZero, instSemigroup, instSemigroupWithZero, instZero, instCommMonoid, instDiv, instGroup, instInv, instMonoid, instZPow, unitClosedBall, unitSphere, unitBall, unitClosedBall, unitSphereToUnits	25
Theorems instContinuousMul, instIsTopologicalGroup, coe_eq_zero, coe_mul, coe_zero, instContinuousMul, instIsCancelMulZero, instIsLeftCancelMulZero, instIsRightCancelMulZero, coe_eq_one, coe_eq_zero, coe_mul, coe_one, coe_pow, coe_zero, instContinuousMul, instIsCancelMulZero, coe_div, coe_inv, coe_mul, coe_one, coe_pow, coe_zpow, coe_unitSphere, unitSphereToUnits_apply_coe, unitSphereToUnits_injective	26
Total	51

Metric.sphere

Definitions

Name	Category	Theorems
instCommGroup 📖	CompOp	—
instHasDistribNeg 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousMul 📖	mathematical	—	ContinuousMul Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Metric.unitSphere.instMonoid	—	Submonoid.continuousMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing
instIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Real Real.instOne instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Metric.unitSphere.instGroup	—	instContinuousMul NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Continuous.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing continuous_subtype_val ne_zero_of_mem_unit_sphere

Metric.unitBall

Definitions

Name	Category	Theorems
instCommSemigroup 📖	CompOp	—
instHasDistribNeg 📖	CompOp	—
instSemigroup 📖	CompOp	2 math math: instContinuousMul, coe_mul
instSemigroupWithZero 📖	CompOp	6 math math: isScalarTower_closedBall_ball_ball, instIsLeftCancelMulZero, instSMulCommClass_sphere_ball_ball, instIsRightCancelMulZero, isScalarTower_sphere_ball_ball, instIsCancelMulZero
instZero 📖	CompOp	5 math math: coe_eq_zero, instIsLeftCancelMulZero, instIsRightCancelMulZero, instIsCancelMulZero, coe_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_zero 📖	mathematical	—	Set Set.instMembership Metric.ball Real Real.instOne Set.Elem instZero	—	Subtype.val_injective coe_zero
coe_mul 📖	mathematical	—	Set Set.instMembership Metric.ball NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne Set.Elem Semigroup.toMul instSemigroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_zero 📖	mathematical	—	Set Set.instMembership Metric.ball Real Real.instOne Set.Elem instZero	—	—
instContinuousMul 📖	mathematical	—	ContinuousMul Set.Elem Metric.ball NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Semigroup.toMul instSemigroup	—	Subsemigroup.continuousMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing
instIsCancelMulZero 📖	mathematical	—	IsCancelMulZero Set.Elem Metric.ball NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne MulZeroClass.toMul SemigroupWithZero.toMulZeroClass instSemigroupWithZero instZero	—	instIsLeftCancelMulZero IsCancelMulZero.toIsLeftCancelMulZero instIsRightCancelMulZero IsCancelMulZero.toIsRightCancelMulZero
instIsLeftCancelMulZero 📖	mathematical	—	IsLeftCancelMulZero Set.Elem Metric.ball NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne MulZeroClass.toMul SemigroupWithZero.toMulZeroClass instSemigroupWithZero instZero	—	Function.Injective.isLeftCancelMulZero Subtype.val_injective
instIsRightCancelMulZero 📖	mathematical	—	IsRightCancelMulZero Set.Elem Metric.ball NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne MulZeroClass.toMul SemigroupWithZero.toMulZeroClass instSemigroupWithZero instZero	—	Function.Injective.isRightCancelMulZero Subtype.val_injective

Metric.unitClosedBall

Definitions

Name	Category	Theorems
instCommMonoid 📖	CompOp	—
instHasDistribNeg 📖	CompOp	—
instMonoid 📖	CompOp	22 math math: Complex.UnitDisc.instSMulCommClass_closedBall_circle, Complex.UnitDisc.instSMulCommClass_closedBall_left, isScalarTower_closedBall_closedBall_closedBall, isScalarTower_sphere_closedBall_closedBall, continuousSMul_closedBall_ball, Complex.UnitDisc.coe_closedBall_smul, instSMulCommClass_sphere_closedBall_closedBall, isScalarTower_closedBall_ball_ball, Complex.UnitDisc.instSMulCommClass_closedBall_right, Complex.UnitDisc.instIsScalarTower_closedBall, isScalarTower_sphere_closedBall_ball, Complex.UnitDisc.coe_smul_closedBall, coe_one, continuousSMul_closedBall_closedBall, instSMulCommClass_closedBall_closedBall_ball, Complex.UnitDisc.instSMulCommClass_circle_closedBall, coe_pow, coe_eq_one, instSMulCommClass_sphere_closedBall_ball, isScalarTower_closedBall_closedBall_ball, instSMulCommClass_closedBall_closedBall_closedBall, Complex.UnitDisc.instIsScalarTower_closedBall_closedBall
instMonoidWithZero 📖	CompOp	2 math math: instIsCancelMulZero, Complex.UnitDisc.instIsScalarTower_closedBall_closedBall
instSemigroup 📖	CompOp	2 math math: coe_mul, instContinuousMul
instSemigroupWithZero 📖	CompOp	—
instZero 📖	CompOp	3 math math: coe_eq_zero, instIsCancelMulZero, coe_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_one 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Set.Elem MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	Subtype.val_injective coe_one
coe_eq_zero 📖	mathematical	—	Set Set.instMembership Metric.closedBall Real Real.instOne Set.Elem instZero	—	Subtype.val_injective coe_zero
coe_mul 📖	mathematical	—	Set Set.instMembership Metric.closedBall NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne Set.Elem Semigroup.toMul instSemigroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_one 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne Set.Elem MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coe_pow 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne Set.Elem Monoid.toNatPow instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	—
coe_zero 📖	mathematical	—	Set Set.instMembership Metric.closedBall Real Real.instOne Set.Elem instZero	—	—
instContinuousMul 📖	mathematical	—	ContinuousMul Set.Elem Metric.closedBall NonUnitalSeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real Real.instOne instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Semigroup.toMul instSemigroup	—	Subsemigroup.continuousMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing
instIsCancelMulZero 📖	mathematical	—	IsCancelMulZero Set.Elem Metric.closedBall SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass instMonoidWithZero instZero	—	Function.Injective.isCancelMulZero Subtype.val_injective

Metric.unitSphere

Definitions

Name	Category	Theorems
instCommMonoid 📖	CompOp	—
instDiv 📖	CompOp	1 math math: coe_div
instGroup 📖	CompOp	1 math math: Metric.sphere.instIsTopologicalGroup
instInv 📖	CompOp	1 math math: coe_inv
instMonoid 📖	CompOp	21 math math: continuousSMul_sphere_ball, coe_one, continuousSMul_sphere_sphere, instSMulCommClass_sphere_sphere_sphere, isScalarTower_sphere_closedBall_closedBall, coe_mul, unitSphereToUnits_apply_coe, unitSphereToUnits_injective, isScalarTower_sphere_sphere_sphere, instSMulCommClass_sphere_closedBall_closedBall, continuousSMul_sphere_closedBall, isScalarTower_sphere_sphere_closedBall, Metric.sphere.instContinuousMul, isScalarTower_sphere_sphere_ball, isScalarTower_sphere_closedBall_ball, instSMulCommClass_sphere_ball_ball, coe_pow, isScalarTower_sphere_ball_ball, instSMulCommClass_sphere_closedBall_ball, instSMulCommClass_sphere_sphere_closedBall, instSMulCommClass_sphere_sphere_ball
instZPow 📖	CompOp	1 math math: coe_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_div 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Real Real.instOne Set.Elem instDiv DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing	—	—
coe_inv 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Real Real.instOne Set.Elem instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing	—	—
coe_mul 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne Set.Elem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_one 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne Set.Elem MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coe_pow 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real Real.instOne Set.Elem Monoid.toNatPow instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	—
coe_zpow 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Real Real.instOne Set.Elem instZPow DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing	—	—

Submonoid

Definitions

Name	Category	Theorems
unitClosedBall 📖	CompOp	—
unitSphere 📖	CompOp	69 math math: Real.hasFDerivAt_fourierChar_neg_bilinear_left, Circle.exp_arg, Circle.injective_arg, Real.fderiv_fourierChar_neg_bilinear_right_apply, Circle.ofConjDivSelf_coe, Circle.starRingEnd_addChar, AddCircle.homeomorphCircle'_symm_apply, rotation_apply, toMatrix_rotation, Complex.UnitDisc.coe_smul_circle, Orientation.rotation_map_complex, BoundedContinuousFunction.mem_charPoly, BoundedContinuousFunction.charAlgHom_apply, Circle.arg_eq_arg, fourier_one, Real.Angle.coe_toCircle, fourier_neg', Circle.smul_def, Circle.ext_iff, Circle.coe_inv_eq_conj, Circle.coe_mul, Real.Angle.arg_toCircle, Circle.coe_pow, Circle.invOn_arg_exp, Circle.star_addChar, Circle.leftInverse_exp_arg, coe_unitSphere, Circle.norm_coe, fourier_apply, Orientation.kahler_rotation_left', rotationOf_coe, Real.hasDerivAt_fourierChar, Orientation.kahler_rotation_left, Circle.coe_eq_one, Real.fourierChar_apply, Circle.coe_inv, Real.differentiable_fourierChar, Circle.normSq_coe, fourier_zero', ZMod.toCircle_intCast, ZMod.toCircle_natCast, Real.deriv_fourierChar, Real.differentiable_fourierChar_neg_bilinear_right, Circle.coeHom_apply, rootsOfUnityCircleEquiv_apply, Circle.coe_inj, Orientation.kahler_rotation_right, fourier_coe_apply', Real.hasFDerivAt_fourierChar_neg_bilinear_right, ZMod.toCircle_apply, Circle.arg_exp, Real.differentiable_fourierChar_neg_bilinear_left, Circle.coe_exp, fourier_add', BoundedContinuousFunction.charMonoidHom_apply, Circle.toUnits_apply, Real.probChar_apply, Circle.coe_injective, Circle.coe_zpow, Circle.coe_div, Circle.coe_one, Real.fderiv_fourierChar_neg_bilinear_left_apply, Circle.argEquiv_apply_coe, Complex.UnitDisc.coe_circle_smul, ZMod.stdAddChar_apply, Circle.argPartialEquiv_apply, MeasureTheory.charFun_eq_integral_probChar, Complex.rotation, BoundedContinuousFunction.char_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_unitSphere 📖	mathematical	—	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing instSetLike unitSphere Metric.sphere SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Real Real.instOne	—	—

Subsemigroup

Definitions

Name	Category	Theorems
unitBall 📖	CompOp	—
unitClosedBall 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
unitSphereToUnits 📖	CompOp	2 math math: unitSphereToUnits_apply_coe, unitSphereToUnits_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
unitSphereToUnits_apply_coe 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing DFunLike.coe MonoidHom Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Real Real.instOne Units MulOneClass.toMulOne Monoid.toMulOneClass Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Units.instMulOneClass MonoidHom.instFunLike unitSphereToUnits Set Set.instMembership	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass
unitSphereToUnits_injective 📖	mathematical	—	Set.Elem Metric.sphere SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Real Real.instOne Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Metric.unitSphere.instMonoid NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Units.instMulOneClass MonoidHom.instFunLike unitSphereToUnits	—	NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass

---

← Back to Index