OrthRadius

📁 Source: Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean

Statistics

Metric	Count
Definitions orthRadius	1
Theorems center_mem_orthRadius_iff, direction_orthRadius, direction_orthRadius_le_iff, dist_sq_eq_iff_mem_orthRadius, dist_sq_eq_of_mem_orthRadius, finrank_orthRadius, instHasOrthogonalProjectionRealDirectionOrthRadius, instNonemptySubtypeMemAffineSubspaceRealOrthRadius, inter_orthRadius_eq_empty_iff, inter_orthRadius_eq_empty_of_finrank_eq_one, inter_orthRadius_eq_empty_of_radius_lt_dist, inter_orthRadius_eq_of_dist_le_radius, inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one, inter_orthRadius_eq_singleton_iff, inter_orthRadius_eq_singleton_of_dist_eq_radius, mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq, mem_inter_orthRadius_iff_vsub_mem_and_norm_sq, mem_orthRadius_iff_inner_left, mem_orthRadius_iff_inner_right, ncard_inter_orthRadius_eq_two_of_dist_lt_radius, ncard_inter_orthRadius_le_two, orthRadius_center, orthRadius_eq_orthRadius_iff, orthRadius_injective, orthRadius_le_orthRadius_iff, orthRadius_map, orthRadius_parallel_orthRadius_iff, orthogonalProjection_orthRadius_center, self_mem_orthRadius, vadd_mem_inter_orthRadius_iff_norm_sq	30
Total	31

EuclideanGeometry.Sphere

Definitions

Name	Category	Theorems
orthRadius 📖	CompOp	39 math math: vadd_mem_inter_orthRadius_iff_norm_sq, inter_orthRadius_eq_of_dist_le_radius, mem_orthRadius_iff_inner_right, IsTangentAt.eq_orthRadius_of_finrank_add_one_eq, isTangent_orthRadius_iff_mem, isTangentAt_orthRadius_iff_mem, Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, Affine.Simplex.affineSpan_faceOpposite_eq_orthRadius_insphere, orthRadius_center, inter_orthRadius_eq_empty_of_finrank_eq_one, orthRadius_eq_orthRadius_iff, Affine.Triangle.affineSpan_pair_eq_orthRadius, ncard_inter_orthRadius_eq_two_of_dist_lt_radius, orthogonalProjection_orthRadius_center, dist_sq_eq_iff_mem_orthRadius, ncard_inter_orthRadius_le_two, mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq, direction_orthRadius_le_iff, IsTangentAt.le_orthRadius, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, IsTangent.eq_orthRadius_or_eq_orthRadius_pointReflection_of_parallel_orthRadius, inter_orthRadius_eq_singleton_iff, center_mem_orthRadius_iff, inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one, inter_orthRadius_eq_empty_of_radius_lt_dist, orthRadius_map, orthRadius_le_orthRadius_iff, mem_inter_orthRadius_iff_vsub_mem_and_norm_sq, inter_orthRadius_eq_empty_iff, mem_tangentSet_iff, orthRadius_injective, inter_orthRadius_eq_singleton_of_dist_eq_radius, direction_orthRadius, orthRadius_parallel_orthRadius_iff, instNonemptySubtypeMemAffineSubspaceRealOrthRadius, instHasOrthogonalProjectionRealDirectionOrthRadius, mem_orthRadius_iff_inner_left, finrank_orthRadius, self_mem_orthRadius

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_mem_orthRadius_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 orthRadius center	—	mem_orthRadius_iff_inner_left neg_vsub_eq_vsub_rev inner_neg_left inner_self_eq_norm_sq_to_K isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
direction_orthRadius 📖	mathematical	—	AffineSubspace.direction Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthRadius 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 center	—	orthRadius.eq_1 AffineSubspace.direction_mk'
direction_orthRadius_le_iff 📖	mathematical	—	Submodule Real Ring.toSemiring Real.instRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthRadius VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup center 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	—	direction_orthRadius Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton
dist_sq_eq_iff_mem_orthRadius 📖	mathematical	—	Real Monoid.toPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center Real.instAdd AffineSubspace Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike orthRadius	—	dist_eq_norm_vsub pow_two vsub_add_vsub_cancel add_comm norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero mem_orthRadius_iff_inner_left
dist_sq_eq_of_mem_orthRadius 📖	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 orthRadius	Real Monoid.toPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center Real.instAdd	—	dist_sq_eq_iff_mem_orthRadius
finrank_orthRadius 📖	mathematical	—	Module.finrank Real Submodule Ring.toSemiring Real.instRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthRadius Real.semiring Submodule.addCommMonoid Submodule.module ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	orthRadius.eq_1 add_comm AffineSubspace.direction_mk' finrank_span_singleton vsub_ne_zero Submodule.finrank_add_finrank_orthogonal
instHasOrthogonalProjectionRealDirectionOrthRadius 📖	mathematical	—	Submodule.HasOrthogonalProjection Real Real.instRCLike AffineSubspace.direction Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthRadius	—	direction_orthRadius Submodule.instHasOrthogonalProjectionOrthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton
instNonemptySubtypeMemAffineSubspaceRealOrthRadius 📖	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 orthRadius	—	orthRadius.eq_1 AffineSubspace.instNonemptySubtypeMemMk'
inter_orthRadius_eq_empty_iff 📖	mathematical	—	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instEmptyCollection Real.instLT Dist.dist PseudoMetricSpace.toDist Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	lt_trichotomy LT.lt.not_gt LT.lt.ne' LE.le.trans_lt dist_nonneg eq_or_ne subsingleton_or_nontrivial AddTorsor.subsingleton_iff Metric.sphere_eq_empty_of_subsingleton orthRadius_center Set.inter_univ Module.finrank_eq_zero_of_subsingleton commRing_strongRankCondition Real.instNontrivial Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule isNoetherian_of_finite Finite.of_subsingleton Module.Projective.of_free not_subsingleton_iff_nontrivial exists_norm_eq EMetric.instNontrivialTopologyOfNontrivial LT.lt.le dist_vadd_left finrank_eq_one_iff' vsub_ne_zero Submodule.span_singleton_eq_top_iff inter_orthRadius_eq_empty_of_finrank_eq_one LT.lt.ne vsub_eq_zero_iff_eq zero_smul smul_smul IsUnit.div_mul_cancel Submodule.exists_mem_ne_zero_of_ne_bot Submodule.orthogonal_eq_bot_iff Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton vadd_mem_inter_orthRadius_iff_norm_sq Submodule.smul_mem norm_smul NormedSpace.toNormSMulClass norm_div norm_norm div_mul_cancel₀ norm_ne_zero_iff sq_abs Real.sq_sqrt sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sq_le_sq Real.instIsStrictOrderedRing abs_of_nonneg LE.le.trans le_abs_self inter_orthRadius_eq_singleton_of_dist_eq_radius dist_self inter_orthRadius_eq_empty_of_radius_lt_dist
inter_orthRadius_eq_empty_of_finrank_eq_one 📖	mathematical	Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instEmptyCollection	—	Set.ext mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq Module.finite_of_finrank_eq_succ commRing_strongRankCondition Real.instNontrivial Module.Free.of_divisionRing Submodule.finrank_add_finrank_orthogonal finrank_span_singleton vsub_ne_zero Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors FiniteDimensional.finiteDimensional_submodule Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Submodule.top_orthogonal_eq_bot vsub_self norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat sub_eq_zero sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_nonneg
inter_orthRadius_eq_empty_of_radius_lt_dist 📖	mathematical	Real Real.instLT radius Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instEmptyCollection	—	Set.ext mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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.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_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.le_of_le_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt mul_pos_of_neg_of_neg IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add Mathlib.Tactic.Linarith.mul_nonpos mul_nonneg_of_nonpos_of_nonpos IsOrderedRing.toMulPosMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT le_of_lt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike
inter_orthRadius_eq_of_dist_le_radius 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius 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 VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instInsert HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.sqrt Real.instSub Monoid.toPow Dist.dist PseudoMetricSpace.toDist Norm.norm NormedAddCommGroup.toNorm Set.instSingletonSet Real.instNeg	—	div_eq_mul_inv smul_smul neg_smul neg_mul inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one Submodule.smul_mem norm_smul NormedSpace.toNormSMulClass norm_inv norm_norm inv_mul_cancel₀ norm_ne_zero_iff
inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius 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 VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor Norm.norm NormedAddCommGroup.toNorm Real.instOne	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instInsert HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid Real.sqrt Real.instSub Monoid.toPow Dist.dist PseudoMetricSpace.toDist Set.instSingletonSet Real.instNeg	—	LE.le.trans dist_nonneg norm_ne_zero_iff NeZero.charZero_one RCLike.charZero_rclike neg_smul finrank_orthRadius FiniteDimensional.of_fact_finrank_eq_two SMulMemClass.smul_mem Submodule.smulMemClass finrank_eq_one_iff_of_nonzero' Fact.out direction_orthRadius sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sq_le_sq Real.instIsStrictOrderedRing abs_of_nonneg le_abs Set.ext vsub_vadd Set.mem_insert_iff Set.mem_singleton_iff vadd_right_cancel_iff AffineSubspace.vsub_right_mem_direction_iff_mem self_mem_orthRadius smul_left_injective IsDomain.toIsCancelMulZero Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.sq_sqrt norm_smul NormedSpace.toNormSMulClass mul_one sq_abs vadd_mem_inter_orthRadius_iff_norm_sq Submodule.smul_mem norm_neg
inter_orthRadius_eq_singleton_iff 📖	mathematical	—	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instSingletonSet Dist.dist PseudoMetricSpace.toDist	—	Set.mem_singleton radius_nonneg_of_mem mem_inter_orthRadius_iff_vsub_mem_and_norm_sq vadd_vsub AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass norm_neg vsub_eq_zero_iff_eq Nat.instAtLeastTwoHAddOfNat smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero two_smul eq_neg_iff_add_eq_zero eq_vadd_iff_vsub_eq inter_orthRadius_eq_singleton_of_dist_eq_radius
inter_orthRadius_eq_singleton_of_dist_eq_radius 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius	Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Set.instSingletonSet	—	Set.ext dist_sq_eq_of_mem_orthRadius instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq 📖	mathematical	—	Set Set.instMembership Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius Real.instLE Real.instZero 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 SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set.instSingletonSet VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Monoid.toPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instSub Dist.dist PseudoMetricSpace.toDist	—	AffineSubspace.vsub_right_mem_direction_iff_mem self_mem_orthRadius sub_eq_iff_eq_add' le_or_gt IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing Nat.instCharZero Nat.instAtLeastTwoHAddOfNat LT.lt.not_ge radius_nonneg_of_mem
mem_inter_orthRadius_iff_vsub_mem_and_norm_sq 📖	mathematical	Real Real.instLE Real.instZero radius	Set Set.instMembership Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius 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 SetLike.instMembership Submodule.setLike Submodule.orthogonal Submodule.span Real.semiring Set.instSingletonSet VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Monoid.toPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instSub Dist.dist PseudoMetricSpace.toDist	—	mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq
mem_orthRadius_iff_inner_left 📖	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 orthRadius Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup center Real.instZero	—	orthRadius.eq_1 AffineSubspace.mem_mk' Submodule.mem_orthogonal_singleton_iff_inner_left
mem_orthRadius_iff_inner_right 📖	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 orthRadius Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup center Real.instZero	—	mem_orthRadius_iff_inner_left inner_eq_zero_symm
ncard_inter_orthRadius_eq_two_of_dist_lt_radius 📖	mathematical	Real Real.instLT Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius	Set.ncard Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius	—	finrank_orthRadius FiniteDimensional.of_fact_finrank_eq_two Fact.out commRing_strongRankCondition Real.instNontrivial Module.Free.of_divisionRing AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass inter_orthRadius_eq_of_dist_le_radius LT.lt.le direction_orthRadius Submodule.norm_coe neg_smul Set.ncard_pair vadd_right_cancel_iff add_eq_zero_iff_eq_neg Nat.instAtLeastTwoHAddOfNat two_smul smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike smul_eq_zero_iff_left div_eq_iff MulZeroClass.zero_mul Real.sqrt_pos sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add sq_lt_sq Real.instIsStrictOrderedRing abs_of_nonneg dist_nonneg lt_abs LT.lt.ne'
ncard_inter_orthRadius_le_two 📖	mathematical	—	Set.ncard Set Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius	—	lt_trichotomy Eq.le ncard_inter_orthRadius_eq_two_of_dist_lt_radius inter_orthRadius_eq_singleton_of_dist_eq_radius Set.ncard_singleton IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat inter_orthRadius_eq_empty_of_radius_lt_dist Set.ncard_empty Nat.instCanonicallyOrderedAdd
orthRadius_center 📖	mathematical	—	orthRadius center 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 AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	vsub_self Submodule.span_zero_singleton Submodule.bot_orthogonal_eq_top AffineSubspace.mk'_top
orthRadius_eq_orthRadius_iff 📖	mathematical	—	orthRadius	—	orthRadius_le_orthRadius_iff Eq.le
orthRadius_injective 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthRadius	—	orthRadius_eq_orthRadius_iff
orthRadius_le_orthRadius_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder orthRadius center	—	AffineSubspace.direction_le Submodule.orthogonal_le direction_orthRadius Submodule.orthogonal_orthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton self_mem_orthRadius mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass sub_mul mul_assoc real_inner_smul_right real_inner_smul_left inner_sub_left vsub_sub_vsub_cancel_right mem_orthRadius_iff_inner_left one_mul vsub_left_cancel_iff one_smul sub_eq_zero vsub_eq_zero_iff_eq zero_smul smul_zero vsub_self instReflLe orthRadius_center
orthRadius_map 📖	mathematical	DFunLike.coe AffineIsometryEquiv Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike center	AffineSubspace.map Real NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Real.normedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineEquiv.toAffineMap AffineIsometryEquiv.toAffineEquiv orthRadius DFunLike.coe AffineIsometryEquiv EquivLike.toFunLike AffineIsometryEquiv.instEquivLike	—	orthRadius.eq_1 RingHomSurjective.ids AffineSubspace.map_mk' RingHomInvPair.ids Submodule.map_span Set.image_congr Set.image_singleton AffineIsometryEquiv.map_vsub Submodule.map_orthogonal_equiv
orthRadius_parallel_orthRadius_iff 📖	mathematical	—	AffineSubspace.Parallel Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthRadius VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup center 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	—	AffineSubspace.direction_mk' Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
orthogonalProjection_orthRadius_center 📖	mathematical	—	AffineSubspace Real NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike orthRadius DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceRealOrthRadius ContinuousAffineMap.instFunLike EuclideanGeometry.orthogonalProjection instHasOrthogonalProjectionRealDirectionOrthRadius center	—	instNonemptySubtypeMemAffineSubspaceRealOrthRadius instHasOrthogonalProjectionRealDirectionOrthRadius Submodule.neg_mem_iff vsub_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass AffineSubspace.direction_mk' Submodule.orthogonal_orthogonal Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton neg_vsub_eq_vsub_rev
self_mem_orthRadius 📖	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 orthRadius	—	AffineSubspace.self_mem_mk'
vadd_mem_inter_orthRadius_iff_norm_sq 📖	mathematical	Real Real.instLE Real.instZero radius 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 VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center	Set Set.instMembership Set.instInter Metric.sphere MetricSpace.toPseudoMetricSpace center radius SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike orthRadius HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Monoid.toPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instSub Dist.dist PseudoMetricSpace.toDist	—	mem_inter_orthRadius_iff_vsub_mem_and_norm_sq vadd_vsub

---

← Back to Index