PerpBisector

📁 Source: Mathlib/Geometry/Euclidean/PerpBisector.lean

Statistics

Metric	Count
Definitions perpBisector	1
Theorems direction_perpBisector, left_mem_perpBisector, mem_perpBisector_iff_dist_eq, mem_perpBisector_iff_dist_eq', mem_perpBisector_iff_inner_eq, mem_perpBisector_iff_inner_eq_inner, mem_perpBisector_iff_inner_eq_zero, mem_perpBisector_iff_inner_eq_zero', mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero, mem_perpBisector_pointReflection_iff_inner_eq_zero, midpoint_mem_perpBisector, perpBisector_comm, perpBisector_eq_top, perpBisector_ne_bot, perpBisector_nonempty, perpBisector_self, right_mem_perpBisector, dist_le_of_wbtw_of_inner_eq_zero, dist_le_of_wbtw_of_mem_perpBisector, dist_lt_of_sbtw_of_inner_eq_zero, dist_lt_of_sbtw_of_mem_perpBisector, inner_vsub_vsub_of_dist_eq_of_dist_eq, mapsTo_perpBisector, preimage_perpBisector	24
Total	25

AffineSubspace

Definitions

Name	Category	Theorems
perpBisector 📖	CompOp	25 math math: Isometry.preimage_perpBisector, mem_perpBisector_iff_inner_eq_zero', left_mem_perpBisector, EuclideanGeometry.preimage_inversion_perpBisector_inversion, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff', mem_perpBisector_iff_inner_eq_zero, perpBisector_nonempty, EuclideanGeometry.preimage_inversion_perpBisector, Isometry.mapsTo_perpBisector, EuclideanGeometry.image_inversion_perpBisector, EuclideanGeometry.image_inversion_sphere_dist_center, EuclideanGeometry.preimage_inversion_sphere_dist_center, mem_perpBisector_iff_inner_eq_inner, perpBisector_comm, mem_perpBisector_iff_dist_eq', perpBisector_eq_top, midpoint_mem_perpBisector, perpBisector_self, mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff, mem_perpBisector_iff_dist_eq, direction_perpBisector, mem_perpBisector_iff_inner_eq, mem_perpBisector_pointReflection_iff_inner_eq_zero, right_mem_perpBisector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
direction_perpBisector 📖	mathematical	—	direction Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace perpBisector Submodule.orthogonal Submodule.span Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set Set.instSingletonSet VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	RCLike.charZero_rclike perpBisector.eq_1 direction_mk' Submodule.ext Submodule.mem_orthogonal_singleton_iff_inner_right
left_mem_perpBisector 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector	—	perpBisector_comm right_mem_perpBisector
mem_perpBisector_iff_dist_eq 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Dist.dist PseudoMetricSpace.toDist	—	dist_eq_norm_vsub real_inner_add_sub_eq_zero_iff vsub_sub_vsub_cancel_left inner_add_left add_eq_zero_iff_eq_neg inner_neg_right neg_vsub_eq_vsub_rev mem_perpBisector_iff_inner_eq_inner
mem_perpBisector_iff_dist_eq' 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Dist.dist PseudoMetricSpace.toDist	—	dist_comm
mem_perpBisector_iff_inner_eq 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike mem_perpBisector_iff_inner_eq_zero vsub_sub_vsub_cancel_right inner_sub_left sub_eq_zero midpoint_vsub_left invOf_eq_inv real_inner_smul_left real_inner_self_eq_norm_sq dist_eq_norm_vsub' div_eq_inv_mul
mem_perpBisector_iff_inner_eq_inner 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	RCLike.charZero_rclike mem_perpBisector_iff_inner_eq_zero add_neg_eq_zero inner_neg_right neg_vsub_eq_vsub_rev inner_add_left Nat.instAtLeastTwoHAddOfNat vsub_midpoint invOf_eq_inv smul_add real_inner_smul_left NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
mem_perpBisector_iff_inner_eq_zero 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup midpoint invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instZero	—	inner_eq_zero_symm RCLike.charZero_rclike
mem_perpBisector_iff_inner_eq_zero' 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup midpoint invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instZero	—	—
mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection Real.instZero	—	RCLike.charZero_rclike mem_perpBisector_iff_inner_eq_zero Equiv.pointReflection_apply Nat.instAtLeastTwoHAddOfNat vsub_midpoint invOf_eq_inv smul_add real_inner_smul_left vadd_vsub_assoc NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
mem_perpBisector_pointReflection_iff_inner_eq_zero 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub Real.instZero	—	RCLike.charZero_rclike mem_perpBisector_iff_inner_eq_zero midpoint_pointReflection_right Equiv.pointReflection_apply vadd_vsub_assoc inner_add_right add_self_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass neg_eq_zero inner_neg_right neg_vsub_eq_vsub_rev
midpoint_mem_perpBisector 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector midpoint invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike	—	RCLike.charZero_rclike vsub_self inner_zero_left
perpBisector_comm 📖	mathematical	—	perpBisector	—	ext
perpBisector_eq_top 📖	mathematical	—	perpBisector Top.top AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	left_mem_perpBisector perpBisector_self
perpBisector_ne_bot 📖	—	—	—	—	nonempty_iff_ne_bot perpBisector_nonempty
perpBisector_nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace instSetLike perpBisector	—	RCLike.charZero_rclike midpoint_mem_perpBisector
perpBisector_self 📖	mathematical	—	perpBisector Top.top AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique vsub_self inner_zero_right
right_mem_perpBisector 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike perpBisector	—	inner_self_eq_norm_sq_to_K vsub_self inner_zero_left isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_le_of_wbtw_of_inner_eq_zero 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instZero	Real.instLE Dist.dist PseudoMetricSpace.toDist	—	dist_sq_lineMap_of_inner_eq_zero dist_sq_of_inner_eq_zero sq_le_one_iff₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr 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 Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le sq_nonneg IsOrderedRing.toPosMulMono Real.sqrt_sq dist_nonneg Real.sqrt_le_sqrt
dist_le_of_wbtw_of_mem_perpBisector 📖	mathematical	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.perpBisector	Real.instLE Dist.dist PseudoMetricSpace.toDist	—	dist_le_of_wbtw_of_inner_eq_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Wbtw.trans_left_right wbtw_midpoint Wbtw.right_mem_image_Ici_of_left_ne vsub_add_vsub_cancel AffineMap.lineMap_vsub_left Nat.instAtLeastTwoHAddOfNat left_vsub_midpoint neg_vsub_eq_vsub_rev smul_neg sub_eq_add_neg inner_sub_right inner_smul_right RCLike.charZero_rclike AffineSubspace.mem_perpBisector_iff_inner_eq_zero MulZeroClass.mul_zero sub_self
dist_lt_of_sbtw_of_inner_eq_zero 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instZero	Real.instLT Dist.dist PseudoMetricSpace.toDist	—	Sbtw.mem_image_Ioo vadd_vsub inner_smul_right NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne' dist_sq_lineMap_of_inner_eq_zero dist_sq_of_inner_eq_zero sq_pos_of_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing dist_pos Sbtw.left_ne_right Real.instIsOrderedRing sq_lt_one_iff₀ Real.instZeroLEOneClass LT.lt.le 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.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 Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Real.sqrt_sq dist_nonneg Real.sqrt_lt_sqrt sq_nonneg IsOrderedRing.toPosMulMono
dist_lt_of_sbtw_of_mem_perpBisector 📖	mathematical	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.perpBisector	Real.instLT Dist.dist PseudoMetricSpace.toDist	—	dist_lt_of_sbtw_of_inner_eq_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Sbtw.trans_left_right sbtw_midpoint_of_ne Sbtw.left_ne Nat.instAtLeastTwoHAddOfNat right_vsub_midpoint inner_smul_right RCLike.charZero_rclike AffineSubspace.mem_perpBisector_iff_inner_eq_zero invOf_eq_inv MulZeroClass.mul_zero
inner_vsub_vsub_of_dist_eq_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor Real.instZero	—	Submodule.mem_orthogonal_singleton_iff_inner_left AffineSubspace.direction_perpBisector AffineSubspace.vsub_mem_direction AffineSubspace.mem_perpBisector_iff_dist_eq'

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapsTo_perpBisector 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace	Set.MapsTo 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	—	Eq.ge preimage_perpBisector
preimage_perpBisector 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace	Set.preimage 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.ext dist_eq

---

← Back to Index