Basic

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

Statistics

Metric	Count
Definitions inversion	1
Theorems inversion, inversion, inversion, inversion, center_eq_inversion, center_eq_inversion', dist_center_inversion, dist_inversion_center, dist_inversion_inversion, dist_inversion_mul_dist_center_eq, inversion_bijective, inversion_def, inversion_dist_center, inversion_dist_center', inversion_eq_center, inversion_eq_center', inversion_eq_lineMap, inversion_injective, inversion_inversion, inversion_involutive, inversion_mul, inversion_of_mem_sphere, inversion_self, inversion_surjective, inversion_vsub_center, inversion_zero_radius, mul_dist_le_mul_dist_add_mul_dist, inversion	28
Total	29

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real Real.pseudoMetricSpace	EuclideanGeometry.inversion	—	continuous_iff_continuousAt ContinuousAt.inversion continuousAt

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real Real.pseudoMetricSpace	EuclideanGeometry.inversion	—	Filter.Tendsto.inversion

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real Real.pseudoMetricSpace	EuclideanGeometry.inversion	—	ContinuousWithinAt.inversion

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real Real.pseudoMetricSpace	EuclideanGeometry.inversion	—	Filter.Tendsto.inversion

EuclideanGeometry

Definitions

Name	Category	Theorems
inversion 📖	CompOp	45 math math: dist_inversion_inversion, inversion_surjective, preimage_inversion_perpBisector_inversion, inversion_of_mem_sphere, inversion_dist_center, inversion_mem_perpBisector_inversion_iff', inversion_vsub_center, inversion_involutive, preimage_inversion_perpBisector, ContDiffAt.inversion, ContinuousWithinAt.inversion, ContinuousOn.inversion, image_inversion_perpBisector, ContDiffOn.inversion, DifferentiableOn.inversion, image_inversion_affineSubspace_of_mem, image_inversion_sphere_dist_center, DifferentiableWithinAt.inversion, preimage_inversion_sphere_dist_center, inversion_inversion, Filter.Tendsto.inversion, inversion_def, inversion_mul, inversion_injective, ContDiff.inversion, center_eq_inversion, hasFDerivAt_inversion, inversion_mem_perpBisector_inversion_iff, Differentiable.inversion, inversion_eq_center, Continuous.inversion, ContDiffWithinAt.inversion, DifferentiableAt.inversion, dist_inversion_mul_dist_center_eq, dist_center_inversion, inversion_eq_center', dist_inversion_center, inversion_dist_center', inversion_zero_radius, mapsTo_inversion_affineSubspace_of_mem, inversion_eq_lineMap, inversion_bijective, inversion_self, ContinuousAt.inversion, center_eq_inversion'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_inversion 📖	mathematical	—	inversion	—	inversion_eq_center
center_eq_inversion' 📖	mathematical	—	inversion Real Real.instZero	—	inversion_eq_center'
dist_center_inversion 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace inversion Real DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid	—	dist_comm dist_inversion_center
dist_inversion_center 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace inversion Real DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid	—	eq_or_ne inversion_self dist_self div_zero dist_ne_zero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons one_mul Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial sq dist_vadd_left norm_smul NormedSpace.toNormSMulClass norm_div norm_mul NormedDivisionRing.toNormMulClass abs_mul_abs_self abs_dist Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_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 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
dist_inversion_inversion 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace inversion Real Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid	—	dist_vadd_cancel_right dist_eq_norm_vsub dist_vsub_cancel_right dist_div_norm_sq_smul vsub_ne_zero
dist_inversion_mul_dist_center_eq 📖	mathematical	—	Real Real.instMul Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace inversion	—	eq_or_ne inversion_zero_radius dist_comm mul_comm inversion_inversion dist_inversion_inversion dist_inversion_center 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.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero dist_ne_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
inversion_bijective 📖	mathematical	—	Function.Bijective inversion	—	Function.Involutive.bijective inversion_involutive
inversion_def 📖	mathematical	—	inversion HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Monoid.toNatPow DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	—
inversion_dist_center 📖	mathematical	—	inversion Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	eq_or_ne inversion_self inversion.eq_1 div_self dist_ne_zero one_pow one_smul vsub_vadd
inversion_dist_center' 📖	mathematical	—	inversion Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	dist_comm inversion_dist_center
inversion_eq_center 📖	mathematical	—	inversion	—	inversion_injective inversion_self
inversion_eq_center' 📖	mathematical	—	inversion Real Real.instZero	—	inversion_zero_radius
inversion_eq_lineMap 📖	mathematical	—	inversion DFunLike.coe AffineMap Real Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.lineMap Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist	—	—
inversion_injective 📖	mathematical	—	inversion	—	Function.Involutive.injective inversion_involutive
inversion_inversion 📖	mathematical	—	inversion	—	eq_or_ne inversion_self inversion.eq_1 dist_inversion_center inversion_vsub_center smul_smul mul_pow div_mul_div_comm div_mul_cancel₀ dist_ne_zero sq div_self pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass one_pow one_smul vsub_vadd
inversion_involutive 📖	mathematical	—	Function.Involutive inversion	—	inversion_inversion
inversion_mul 📖	mathematical	—	inversion Real Real.instMul DFunLike.coe AffineMap CommRing.toRing Real.commRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.homothety Monoid.toNatPow Real.instMonoid	—	mul_div_assoc mul_pow
inversion_of_mem_sphere 📖	mathematical	Set Set.instMembership Metric.sphere MetricSpace.toPseudoMetricSpace	inversion	—	inversion_dist_center Membership.mem.out
inversion_self 📖	mathematical	—	inversion	—	dist_self div_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat vsub_self smul_zero zero_vadd
inversion_surjective 📖	mathematical	—	inversion	—	Function.Involutive.surjective inversion_involutive
inversion_vsub_center 📖	mathematical	—	VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace inversion Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace 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 Monoid.toNatPow DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist	—	vadd_vsub
inversion_zero_radius 📖	mathematical	—	inversion Real Real.instZero	—	zero_div zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat zero_smul zero_vadd
mul_dist_le_mul_dist_add_mul_dist 📖	mathematical	—	Real Real.instLE Real.instMul Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real.instAdd	—	eq_or_ne dist_self MulZeroClass.zero_mul zero_add le_refl add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_nonneg MulZeroClass.mul_zero add_zero dist_comm mul_comm dist_triangle div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing mul_pos IsStrictOrderedRing.toPosMulStrictMono dist_pos one_div mul_inv_rev Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt 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.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt one_pow dist_inversion_inversion

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inversion 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real Real.pseudoMetricSpace	EuclideanGeometry.inversion	—	vadd IsTopologicalAddTorsor.toContinuousVAdd instIsTopologicalAddTorsor_1 smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal dist dist_ne_zero vsub

---

← Back to Index