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, finrank_orthRadius, mem_orthRadius_iff_inner_left, mem_orthRadius_iff_inner_right, orthRadius_center, orthRadius_eq_orthRadius_iff, orthRadius_le_orthRadius_iff, orthRadius_map, orthRadius_parallel_orthRadius_iff, self_mem_orthRadius	12
Total	13

EuclideanGeometry.Sphere

Definitions

Name	Category	Theorems
orthRadius 📖	CompOp	21 math math: 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, orthRadius_eq_orthRadius_iff, Affine.Triangle.affineSpan_pair_eq_orthRadius, direction_orthRadius_le_iff, IsTangentAt.le_orthRadius, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, center_mem_orthRadius_iff, orthRadius_map, orthRadius_le_orthRadius_iff, mem_tangentSet_iff, direction_orthRadius, orthRadius_parallel_orthRadius_iff, 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
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
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
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_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 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 NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor AffineEquiv.toAffineMap AffineIsometryEquiv.toAffineEquiv orthRadius	—	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
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'

---

← Back to Index