Sphere

📁 Source: Mathlib/Geometry/Manifold/Instances/Sphere.lean

Statistics

Metric	Count
Definitions instChartedSpaceSphere, instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere, instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle, stereoInvFun, stereoInvFunAux, stereoToFun, stereographic, stereographic'	8
Theorems codRestrict_sphere, instIsManifoldSphere, contDiffOn_stereoToFun, contDiff_stereoInvFunAux, contMDiff_circleExp, contMDiff_coe_sphere, contMDiff_neg_sphere, continuousOn_stereoToFun, continuous_stereoInvFun, finrank_real_complex_fact', hasFDerivAt_stereoInvFunAux, hasFDerivAt_stereoInvFunAux_comp_coe, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, isOpenEmbedding_stereographic_symm, mfderiv_coe_sphere_injective, range_mfderiv_coe_sphere, range_stereographic_symm, sphere_ext_iff, stereoInvFunAux_apply, stereoInvFunAux_mem, stereoInvFun_apply, stereoInvFun_ne_north_pole, stereoToFun_apply, stereo_left_inv, stereo_right_inv, stereographic'_source, stereographic'_symm_apply, stereographic'_target, stereographic_apply, stereographic_apply_neg, stereographic_neg_apply, stereographic_source, stereographic_target, surjective_stereographic	36
Total	44

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict_sphere 📖	mathematical	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf chartedSpaceSelf Set Set.instMembership Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Set.Elem instTopologicalSpaceSubtype EuclideanSpace.instChartedSpaceSphere Set.codRestrict	—	fact_one_le_two_ennreal contMDiff_iff_target IsManifold.instOfTopWithTopENat EuclideanSpace.instIsManifoldSphere continuous_induced_rng continuous RingHomInvPair.ids ne_zero_of_mem_unit_sphere IsScalarTower.left ContDiff.contDiffOn LinearIsometryEquiv.contDiff SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContDiffOn.contMDiffOn ContDiffOn.comp_inter contDiffOn_stereoToFun contMDiffOn Set.ext sub_zero inner_eq_one_iff_of_norm_eq_one norm_eq_of_mem_sphere PartialEquiv.trans_refl stereographic'_source inner_neg_right real_inner_comm instIsTopologicalAddGroupReal map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass instIsTopologicalRingReal SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Set.inter_univ Set.univ_inter ContMDiffOn.comp' ContMDiffOn.of_le le_top

EuclideanSpace

Definitions

Name	Category	Theorems
instChartedSpaceSphere 📖	CompOp	6 math math: contMDiff_neg_sphere, contMDiff_coe_sphere, instIsManifoldSphere, mfderiv_coe_sphere_injective, range_mfderiv_coe_sphere, ContMDiff.codRestrict_sphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsManifoldSphere 📖	mathematical	—	IsManifold Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Top.top WithTop ENat WithTop.top Set.Elem Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne instTopologicalSpaceSubtype Set Set.instMembership instChartedSpaceSphere	—	isManifold_of_contDiffOn fact_one_le_two_ennreal RingHomInvPair.ids ne_zero_of_mem_unit_sphere IsScalarTower.left SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContDiff.comp_contDiffOn LinearIsometryEquiv.contDiff contDiffOn_stereoToFun ContDiff.comp contDiff_stereoInvFunAux ContinuousLinearMap.contDiff stereographic'_target stereographic'_source Set.univ_inter Set.range_id Set.inter_univ real_inner_comm ContDiffOn.comp_inter ContDiff.contDiffOn

(root)

Definitions

Name	Category	Theorems
instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere 📖	CompOp	1 math math: instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere
instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle 📖	CompOp	3 math math: instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, contMDiff_circleExp
stereoInvFun 📖	CompOp	4 math math: stereo_left_inv, stereoInvFun_apply, stereo_right_inv, continuous_stereoInvFun
stereoInvFunAux 📖	CompOp	5 math math: hasFDerivAt_stereoInvFunAux, stereoInvFunAux_apply, stereoInvFunAux_mem, contDiff_stereoInvFunAux, hasFDerivAt_stereoInvFunAux_comp_coe
stereoToFun 📖	CompOp	5 math math: continuousOn_stereoToFun, stereo_left_inv, contDiffOn_stereoToFun, stereoToFun_apply, stereo_right_inv
stereographic 📖	CompOp	8 math math: stereographic_apply_neg, range_stereographic_symm, isOpenEmbedding_stereographic_symm, stereographic_neg_apply, stereographic_target, stereographic_source, stereographic_apply, surjective_stereographic
stereographic' 📖	CompOp	3 math math: stereographic'_source, stereographic'_target, stereographic'_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_stereoToFun 📖	mathematical	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Submodule.normedAddCommGroup Real.instRing Submodule.normedSpace Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id NontriviallyNormedField.toNormedField IsScalarTower.left Real.instMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.normedField stereoToFun setOf DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace ContinuousLinearMap.funLike Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing innerSL Real.instOne	—	ContDiffOn.fun_smul IsScalarTower.left NormedSpace.toIsBoundedSMul Submodule.isScalarTower' SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContDiffOn.div ContDiff.contDiffOn contDiff_const ContDiff.sub ContinuousLinearMap.contDiff sub_eq_zero Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton
contDiff_stereoInvFunAux 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup stereoInvFunAux	—	contDiff_norm_sq Nat.instAtLeastTwoHAddOfNat ContDiff.inv ContDiff.add contDiff_const Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono sub_eq_zero_of_eq ContDiff.smul NormedSpace.toIsBoundedSMul IsScalarTower.left contDiff_id ContDiff.sub ContDiff.of_le le_top
contMDiff_circleExp 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Circle instTopologicalSpaceCircle instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle DFunLike.coe ContinuousMap ContinuousMap.instFunLike Circle.exp	—	ContMDiff.codRestrict_sphere ContMDiffAdd.toIsManifold instContMDiffAddSelf finrank_real_complex_fact' ContDiff.contMDiff ContDiff.comp Complex.contDiff_exp ContDiff.smul NormedSpace.toIsBoundedSMul IsScalarTower.left contDiff_id contDiff_const
contMDiff_coe_sphere 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Set Set.instMembership Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne instTopologicalSpaceSubtype EuclideanSpace.instChartedSpaceSphere chartedSpaceSelf	—	fact_one_le_two_ennreal contMDiff_iff IsManifold.instOfTopWithTopENat EuclideanSpace.instIsManifoldSphere ContMDiffAdd.toIsManifold instContMDiffAddSelf continuous_subtype_val RingHomInvPair.ids ne_zero_of_mem_unit_sphere ContDiff.contDiffOn IsScalarTower.left ContDiff.comp contDiff_stereoInvFunAux ContinuousLinearMap.contDiff LinearIsometryEquiv.contDiff
contMDiff_neg_sphere 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Set.Elem Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne instTopologicalSpaceSubtype Set Set.instMembership EuclideanSpace.instChartedSpaceSphere InvolutiveNeg.toNeg instInvolutiveNegElemSphereOfNat	—	ContMDiff.codRestrict_sphere fact_one_le_two_ennreal IsManifold.instOfTopWithTopENat EuclideanSpace.instIsManifoldSphere ContMDiff.comp ContDiff.contMDiff contDiff_neg contMDiff_coe_sphere
continuousOn_stereoToFun 📖	mathematical	—	ContinuousOn Submodule Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet instTopologicalSpaceSubtype stereoToFun setOf DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace ContinuousLinearMap.funLike CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing innerSL Real.instOne	—	ContDiffOn.continuousOn IsScalarTower.left SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul contDiffOn_stereoToFun
continuous_stereoInvFun 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Continuous Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Set.Elem Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup instTopologicalSpaceSubtype Set.instMembership stereoInvFun	—	continuous_induced_rng Continuous.comp ContDiff.continuous contDiff_stereoInvFunAux continuous_subtype_val
finrank_real_complex_fact' 📖	mathematical	—	Fact Module.finrank Real Complex Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex	—	Complex.finrank_real_complex_fact
hasFDerivAt_stereoInvFunAux 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace stereoInvFunAux ContinuousLinearMap.id Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul map_zero AddMonoidHomClass.toZeroHomClass instIsTopologicalRingReal DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smul_zero AddMonoid.continuousConstSMul_nat AddMonoid.nat_smulCommClass' HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt_norm_sq Nat.instAtLeastTwoHAddOfNat RingHomCompTriple.ids ContinuousMul.to_continuousSMul IsTopologicalAddGroup.toContinuousAdd ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.toSpanSingleton.congr_simp norm_zero zero_pow Nat.instCharZero zero_add add_zero ContinuousLinearMap.comp_zero HasFDerivAt.comp hasFDerivAt_inv RCLike.charZero_rclike HasFDerivAt.add hasFDerivAt_const smulCommClass_self IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass IsScalarTower.left IsBoundedSMul.continuousSMul ContinuousLinearMap.ext zero_sub ContinuousLinearMap.smulRight.congr_simp sub_self zero_smul HasFDerivAt.smul hasFDerivAt_id HasFDerivAt.sub inv_smul_smul₀ neg_smul smul_neg neg_zero
hasFDerivAt_stereoInvFunAux_comp_coe 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Submodule.addCommGroup Real.instRing SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype stereoInvFunAux Submodule.subtypeL Submodule.zero	—	hasFDerivAt_stereoInvFunAux HasFDerivAt.comp IsScalarTower.left ContinuousLinearMap.hasFDerivAt
instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere 📖	mathematical	—	IsManifold Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Top.top WithTop ENat WithTop.top Set.Elem Metric.sphere PiLp.instPseudoMetricSpace Real.pseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Real.instOne instTopologicalSpaceSubtype Set Set.instMembership PiLp.topologicalSpace instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere	—	EuclideanSpace.instIsManifoldSphere fact_one_le_two_ennreal
instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle 📖	mathematical	—	IsManifold Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Top.top WithTop ENat WithTop.top Circle instTopologicalSpaceCircle instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle	—	EuclideanSpace.instIsManifoldSphere finrank_real_complex_fact'
instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle 📖	mathematical	—	LieGroup Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal modelWithCornersSelf Top.top WithTop ENat WithTop.top Circle CommGroup.toGroup Circle.instCommGroup instTopologicalSpaceCircle instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle	—	fact_one_le_two_ennreal instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle ContMDiff.codRestrict_sphere IsManifold.prod finrank_real_complex_fact' NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass contMDiff_iff ContMDiffAdd.toIsManifold instContMDiffAddSelf continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContDiff.contDiffOn contDiff_mul ContMDiff.prodMap contMDiff_coe_sphere ContMDiff.comp Circle.coe_inv_eq_conj RingHomInvPair.ids ContDiff.contMDiff ContinuousLinearEquiv.contDiff
isOpenEmbedding_stereographic_symm 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Topology.IsOpenEmbedding Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Set.Elem Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup instTopologicalSpaceSubtype Set.instMembership OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm stereographic	—	OpenPartialHomeomorph.to_isOpenEmbedding
mfderiv_coe_sphere_injective 📖	mathematical	—	TangentSpace Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Set Set.instMembership Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne instTopologicalSpaceSubtype EuclideanSpace.instChartedSpaceSphere chartedSpaceSelf DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv	—	fact_one_le_two_ennreal MDifferentiableAt.mfderiv ContMDiffAt.mdifferentiableAt contMDiff_coe_sphere one_ne_zero NeZero.charZero_one WithTop.charZero PartialEquiv.trans_refl Set.range_id fderivWithin_univ RingHomInvPair.ids ne_zero_of_mem_unit_sphere map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass hasFDerivAt_stereoInvFunAux_comp_coe IsScalarTower.left RingHomCompTriple.ids HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul PiLp.instIsBoundedSMul Real.isBoundedSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivAt.comp ContinuousLinearEquiv.hasFDerivAt ContinuousLinearMap.coe_comp' ContinuousLinearEquiv.coe_coe Subtype.val_injective
range_mfderiv_coe_sphere 📖	mathematical	—	LinearMap.range Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Set Set.instMembership Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne instTopologicalSpaceSubtype EuclideanSpace.instChartedSpaceSphere chartedSpaceSelf DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap mfderiv Submodule.orthogonal Submodule.span Real.semiring NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.instSingletonSet	—	fact_one_le_two_ennreal RingHomSurjective.ids MDifferentiableAt.mfderiv ContMDiffAt.mdifferentiableAt contMDiff_coe_sphere one_ne_zero NeZero.charZero_one WithTop.charZero LinearMap.range.congr_simp Set.range_id fderivWithin_univ RingHomInvPair.ids ne_zero_of_mem_unit_sphere map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass hasFDerivAt_stereoInvFunAux_comp_coe IsScalarTower.left RingHomCompTriple.ids Submodule.range_subtype Submodule.span_eq_span Submodule.neg_mem_iff Submodule.mem_span_singleton_self LinearEquiv.range_comp HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul PiLp.instIsBoundedSMul Real.isBoundedSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivAt.comp ContinuousLinearEquiv.hasFDerivAt
range_stereographic_symm 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne Set Set.instMembership Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Set.range Set.Elem Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set.instSingletonSet OpenPartialHomeomorph.toFun' instTopologicalSpaceSubtype OpenPartialHomeomorph.symm stereographic Compl.compl Set.instCompl	—	le_antisymm OpenPartialHomeomorph.map_target PartialEquiv.target_subset_range
sphere_ext_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	norm_eq_of_mem_sphere
stereoInvFunAux_apply 📖	mathematical	—	stereoInvFunAux Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instInv Real.instAdd Monoid.toNatPow Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Real.instSub	—	—
stereoInvFunAux_mem 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet	Set.instMembership Metric.sphere NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup stereoInvFunAux	—	Nat.instAtLeastTwoHAddOfNat Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE even_two_mul Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo norm_add_sq_real norm_smul NormedSpace.toNormSMulClass Real.norm_ofNat mul_pow inner_smul_right inner_smul_left conj_trivial instTrivialStarReal Submodule.mem_orthogonal_singleton_iff_inner_left MulZeroClass.mul_zero add_zero mul_one sq_abs Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isNat_mul abs_norm abs_of_pos abs_inv inv_mul_cancel₀ LT.lt.ne'
stereoInvFun_apply 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Set Set.instMembership Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup stereoInvFun SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instInv Real.instAdd Monoid.toNatPow Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Set.instSingletonSet Submodule.normedAddCommGroup Real.instRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Real.instSub	—	—
stereoInvFun_ne_north_pole 📖	—	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	—	—	Subtype.coe_ne_coe inner_lt_one_iff_real_of_norm_eq_one Nat.instAtLeastTwoHAddOfNat smul_add sub_zero stereoInvFunAux_mem Submodule.mem_orthogonal_singleton_iff_inner_right inv_mul_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le real_inner_comm inner_add_right inner_smul_right MulZeroClass.mul_zero inner_self_eq_norm_sq_to_K one_pow mul_one zero_add
stereoToFun_apply 📖	mathematical	—	stereoToFun Real Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Submodule.smul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace ContinuousLinearMap.funLike Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing innerSL instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module Submodule.orthogonalProjection Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Real.instDivisionRing	—	—
stereo_left_inv 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	stereoInvFun stereoToFun Set Set.instMembership Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	IsScalarTower.left Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton smul_add Submodule.starProjection_add_starProjection_orthogonal Submodule.starProjection_unit_singleton Submodule.mem_orthogonal_singleton_iff_inner_right inner_smul_left MulZeroClass.mul_zero norm_eq_of_mem_sphere mul_one norm_smul NormedSpace.toNormSMulClass sq_abs sq norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero inner_lt_one_iff_real_of_norm_eq_one lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Submodule.coe_smul_of_tower norm_div RCLike.norm_ofNat abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add mul_nonneg IsOrderedRing.toPosMulMono le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul mul_pos Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero
stereo_right_inv 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	stereoToFun Set Set.instMembership Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup stereoInvFun	—	IsScalarTower.left smul_add map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass Submodule.orthogonalProjection_mem_subspace_eq_self Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero Submodule.mem_orthogonal_singleton_iff_inner_right inner_self_eq_norm_sq_to_K one_pow Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.zero_eq_eval add_zero Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one MulZeroClass.mul_zero mul_one zero_add Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero add_sub_sub_cancel NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike ZeroLEOneClass.neZero.four Real.instZeroLEOneClass NeZero.charZero_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add
stereographic'_source 📖	mathematical	—	PartialEquiv.source Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne EuclideanSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Real.pseudoMetricSpace stereographic' Compl.compl Set.instCompl Set.instSingletonSet	—	Subtype.coe_eta Set.inter_univ
stereographic'_symm_apply 📖	mathematical	—	Set Set.instMembership Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne OpenPartialHomeomorph.toFun' EuclideanSpace Set.Elem PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceSubtype OpenPartialHomeomorph.symm stereographic'	—	RingHomInvPair.ids fact_one_le_two_ennreal ne_zero_of_mem_unit_sphere Nat.instAtLeastTwoHAddOfNat Subtype.coe_eta stereo_right_inv LinearIsometryEquiv.norm_map smul_add
stereographic'_target 📖	mathematical	—	PartialEquiv.target Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne EuclideanSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Real.pseudoMetricSpace stereographic' Set.univ	—	Set.inter_self
stereographic_apply 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	OpenPartialHomeomorph.toFun' Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet instTopologicalSpaceSubtype Set.instMembership stereographic Submodule.smul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.normedField IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike Submodule.orthogonalProjection Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Real.instDivisionRing SeminormedAddCommGroup.toAddCommGroup	—	—
stereographic_apply_neg 📖	mathematical	—	OpenPartialHomeomorph.toFun' Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Set.instMembership SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup instTopologicalSpaceSubtype stereographic norm_eq_of_mem_sphere InvolutiveNeg.toNeg instInvolutiveNegElemSphereOfNat Submodule.zero	—	norm_eq_of_mem_sphere IsScalarTower.left Nat.instAtLeastTwoHAddOfNat Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton inner_neg_right inner_self_eq_norm_sq_to_K one_pow sub_neg_eq_add map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero neg_zero smul_zero
stereographic_neg_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet Set.instMembership SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup InvolutiveNeg.toNeg instInvolutiveNegElemSphereOfNat instTopologicalSpaceSubtype stereographic norm_eq_of_mem_sphere Submodule.zero	—	norm_eq_of_mem_sphere neg_neg stereographic_apply_neg
stereographic_source 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	PartialEquiv.source Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set.instMembership stereographic Compl.compl Set.instCompl	—	—
stereographic_target 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	PartialEquiv.target Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set.instMembership stereographic Set.univ	—	—
surjective_stereographic 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	Set.Elem Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet OpenPartialHomeomorph.toFun' instTopologicalSpaceSubtype Set.instMembership stereographic	—	PartialEquiv.surjective_of_target_eq_univ

---

← Back to Index