ImageHyperplane

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

Statistics

Metric	Count
Definitions	0
Theorems image_inversion_affineSubspace_of_mem, image_inversion_perpBisector, image_inversion_sphere_dist_center, inversion_mem_perpBisector_inversion_iff, inversion_mem_perpBisector_inversion_iff', mapsTo_inversion_affineSubspace_of_mem, preimage_inversion_perpBisector, preimage_inversion_perpBisector_inversion, preimage_inversion_sphere_dist_center	9
Total	9

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_inversion_affineSubspace_of_mem 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Set.image inversion SetLike.coe	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.MapsTo.image_subset mapsTo_inversion_affineSubspace_of_mem inversion_inversion
image_inversion_perpBisector 📖	mathematical	—	Set.image inversion SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike AffineSubspace.perpBisector Set Set.instSDiff Metric.sphere DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Set.instSingletonSet	—	Set.image_eq_preimage_of_inverse inversion_involutive preimage_inversion_perpBisector
image_inversion_sphere_dist_center 📖	mathematical	—	Set.image inversion Metric.sphere MetricSpace.toPseudoMetricSpace Dist.dist PseudoMetricSpace.toDist Set Set.instInsert SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike AffineSubspace.perpBisector	—	Set.image_eq_preimage_of_inverse inversion_involutive preimage_inversion_sphere_dist_center
inversion_mem_perpBisector_inversion_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.perpBisector inversion Dist.dist PseudoMetricSpace.toDist	—	AffineSubspace.mem_perpBisector_iff_dist_eq 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.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.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul 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 Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
inversion_mem_perpBisector_inversion_iff' 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.perpBisector inversion Dist.dist PseudoMetricSpace.toDist	—	eq_or_ne inversion_self inversion_mem_perpBisector_inversion_iff
mapsTo_inversion_affineSubspace_of_mem 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Set.MapsTo inversion SetLike.coe	—	AffineMap.lineMap_mem
preimage_inversion_perpBisector 📖	mathematical	—	Set.preimage inversion SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike AffineSubspace.perpBisector Set Set.instSDiff Metric.sphere DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Set.instSingletonSet	—	dist_inversion_center preimage_inversion_perpBisector_inversion inversion_inversion
preimage_inversion_perpBisector_inversion 📖	mathematical	—	Set.preimage inversion SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike AffineSubspace.perpBisector Set Set.instSDiff Metric.sphere Dist.dist PseudoMetricSpace.toDist Set.instSingletonSet	—	Set.ext inversion_mem_perpBisector_inversion_iff'
preimage_inversion_sphere_dist_center 📖	mathematical	—	Set.preimage inversion Metric.sphere MetricSpace.toPseudoMetricSpace Dist.dist PseudoMetricSpace.toDist Set Set.instInsert SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike AffineSubspace.perpBisector	—	Set.ext eq_or_ne inversion_self dist_comm Set.mem_preimage Metric.mem_sphere inversion_mem_perpBisector_inversion_iff inversion_inversion

---

← Back to Index