Calculus

📁 Source: Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

Statistics

Metric	Count
Definitions	0
Theorems inversion, inversion, inversion, inversion, inversion, inversion, inversion, inversion, hasFDerivAt_inversion	9
Total	9

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat Real.normedAddCommGroup RCLike.toInnerProductSpaceReal	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	contDiff_iff_contDiffAt ContDiffAt.inversion contDiffAt

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat Real.normedAddCommGroup RCLike.toInnerProductSpaceReal	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	ContDiffWithinAt.inversion

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat Real.normedAddCommGroup RCLike.toInnerProductSpaceReal	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	ContDiffWithinAt.inversion

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat Real.normedAddCommGroup RCLike.toInnerProductSpaceReal	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	add smul NormedSpace.toIsBoundedSMul IsScalarTower.left pow div dist dist_ne_zero sub

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	DifferentiableAt.inversion

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	differentiableWithinAt_univ DifferentiableWithinAt.inversion

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	DifferentiableWithinAt.inversion

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace	EuclideanGeometry.inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	add smul NormedSpace.toIsBoundedSMul IsScalarTower.left pow mul inv dist dist_ne_zero sub

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFDerivAt_inversion 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace inversion NormedAddCommGroup.toMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.normedField smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul Monoid.toNatPow DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids LinearIsometryEquiv.toContinuousLinearEquiv Submodule.reflection Submodule.orthogonal Submodule.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Real.instDivisionRing	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton add_left_surjective IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass IsScalarTower.left IsBoundedSMul.continuousSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RingHomIsometric.ids RingHomCompTriple.ids IsTopologicalSemiring.toContinuousAdd dist_eq_norm div_pow div_eq_mul_inv HasFDerivAt.sub_const hasFDerivAt_id HasFDerivAt.const_mul HasDerivAt.comp_hasFDerivAt hasDerivAt_inv add_sub_cancel_left isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat AddLeftCancelSemigroup.toIsLeftCancelAdd HasFDerivAt.norm_sq HasFDerivAt.add_const HasFDerivAt.smul HasFDerivAt.congr_fderiv LinearMap.ext_on_codisjoint ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsCompl.codisjoint Submodule.isCompl_orthogonal_of_hasOrthogonalProjection LinearMap.eqOn_span' div_eq_inv_mul sq div_self_mul_self' instIsUniformAddGroupReal instIsTopologicalRingReal instIsTopologicalAddGroupReal ContinuousLinearMap.smulRight.congr_simp ContinuousLinearMap.comp.congr_simp ContinuousLinearMap.comp_id neg_smul smul_neg dist_self_add_left mul_pow inv_pow Submodule.reflection.congr_simp inner_self_eq_norm_sq_to_K nsmul_eq_mul two_mul mul_add Distrib.leftDistribClass neg_add_rev add_smul add_neg_cancel_comm_assoc Submodule.reflection_orthogonalComplement_singleton_eq_neg Submodule.mem_orthogonal_singleton_iff_inner_right MulZeroClass.mul_zero neg_zero zero_smul add_zero Submodule.reflection_mem_subspace_eq_self

---

← Back to Index