Basic

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

Statistics

Metric	Count
Definitions Concyclic, Cospherical, IsDiameter, center, ofDiameter, radius, instCoeSphereSet, instMembershipSphere	8
Theorems Coplanar, Cospherical, subset, affineIndependent, affineIndependent_of_mem_of_ne, affineIndependent_of_ne, inclusion, inclusion_iff, subset, subtype_val, subtype_val_iff, dist_left_right, dist_left_right_div_two, left_eq_of_isDiameter, left_eq_right_iff, left_mem, left_ne_right_iff_radius_ne_zero, left_ne_right_iff_radius_pos, midpoint_eq_center, ofDiameter_eq, pointReflection_center_left, pointReflection_center_right, right_eq_of_isDiameter, right_mem, sbtw, wbtw, center_eq_iff_eq_of_mem, center_mem_iff, center_ne_iff_ne_of_mem, coe_mk, cospherical, dist_center_lt_radius_of_sbtw, dist_center_midpoint_lt_radius, ext, ext_iff, inner_vsub_center_midpoint_vsub, isDiameter_comm, isDiameter_iff_left_mem_and_midpoint_eq_center, isDiameter_iff_left_mem_and_pointReflection_center_left, isDiameter_iff_mem_and_mem_and_dist, isDiameter_iff_mem_and_mem_and_wbtw, isDiameter_iff_ofDiameter_eq, isDiameter_iff_right_mem_and_midpoint_eq_center, isDiameter_iff_right_mem_and_pointReflection_center_right, isDiameter_ofDiameter, mem_coe, mem_coe', mk_center, mk_center_radius, mk_radius, ne_iff, nonempty_iff, radius_nonneg_of_mem, concyclic_empty, concyclic_pair, concyclic_singleton, cospherical_def, cospherical_empty, cospherical_iff_exists_sphere, cospherical_pair, cospherical_singleton, dist_center_eq_dist_center_of_mem_sphere, dist_center_eq_dist_center_of_mem_sphere', dist_of_mem_subset_mk_sphere, dist_of_mem_subset_sphere, eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two, eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two, inner_nonneg_of_dist_le_radius, inner_pos_of_dist_lt_radius, inner_pos_or_eq_of_dist_le_radius, inner_vsub_center_vsub_pos, inner_vsub_vsub_of_mem_sphere_of_mem_sphere, instNonemptySphere, mem_sphere, mem_sphere', sbtw_of_collinear_of_dist_center_lt_radius, subset_sphere, wbtw_of_collinear_of_dist_center_le_radius, cospherical	79
Total	87

EuclideanGeometry

Definitions

Name	Category	Theorems
Concyclic 📖	CompData	6 math math: Concyclic.subset, concyclic_empty, concyclic_of_two_zsmul_oangle_eq_of_not_collinear, concyclic_pair, concyclic_or_collinear_of_two_zsmul_oangle_eq, concyclic_singleton
Cospherical 📖	MathDef	18 math math: Cospherical.subtype_val_iff, Cospherical.subset, Cospherical.inclusion_iff, Cospherical.inclusion, cospherical_pair, cospherical_def, cospherical_singleton, cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi, Sphere.cospherical, cospherical_or_collinear_of_two_zsmul_oangle_eq, cospherical_iff_exists_mem_of_complete, cospherical_of_two_zsmul_oangle_eq_of_not_collinear, Concyclic.Cospherical, Cospherical.subtype_val, cospherical_iff_exists_mem_of_finiteDimensional, cospherical_iff_exists_sphere, Isometry.cospherical, cospherical_empty
instCoeSphereSet 📖	CompOp	—
instMembershipSphere 📖	CompOp	41 math math: subset_sphere, Sphere.thales_theorem, Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center, Sphere.secondInter_mem, Sphere.IsExtTangentAt.mem_left, Affine.Simplex.mem_circumsphere, Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem, Sphere.isTangent_orthRadius_iff_mem, Sphere.isDiameter_iff_right_mem_and_pointReflection_center_right, Sphere.isTangentAt_orthRadius_iff_mem, Sphere.IsDiameter.right_mem, Sphere.IsDiameter.left_mem, Affine.Triangle.altitudeFoot_mem_ninePointCircle, Affine.Simplex.eulerPoint_mem_ninePointCircle, Sphere.isExtTangentAt_center_iff, Affine.Simplex.ExcenterExists.touchpoint_mem_exsphere, Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq, Sphere.power_eq_zero_iff_mem_sphere, Sphere.IsTangentAt.mem_and_mem_iff_eq, Sphere.isIntTangentAt_self_iff_mem, mem_sphere, Sphere.IsIntTangentAt.mem_left, mem_sphere', Sphere.mem_coe, Sphere.isDiameter_iff_mem_and_mem_and_dist, Sphere.IsTangentAt.mem_sphere, Sphere.isDiameter_iff_mem_and_mem_and_wbtw, Sphere.IsExtTangentAt.mem_right, Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle, Sphere.isIntTangentAt_center_iff, Sphere.mem_tangentSet_iff, Sphere.mem_coe', Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, Sphere.IsIntTangentAt.mem_right, Sphere.center_mem_iff, Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center, Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter, Sphere.isDiameter_iff_left_mem_and_pointReflection_center_left, Sphere.eq_or_eq_secondInter_iff_mem_of_mem_affineSpan_pair, Affine.Simplex.touchpoint_mem_insphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concyclic_empty 📖	mathematical	—	Concyclic Set Set.instEmptyCollection	—	cospherical_empty AddTorsor.nonempty coplanar_empty
concyclic_pair 📖	mathematical	—	Concyclic Set Set.instInsert Set.instSingletonSet	—	cospherical_pair coplanar_pair
concyclic_singleton 📖	mathematical	—	Concyclic Set Set.instSingletonSet	—	cospherical_singleton coplanar_singleton
cospherical_def 📖	mathematical	—	Cospherical Real Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	—
cospherical_empty 📖	mathematical	—	Cospherical Set Set.instEmptyCollection	—	—
cospherical_iff_exists_sphere 📖	mathematical	—	Cospherical Sphere Set Set.instHasSubset Metric.sphere MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	—	—
cospherical_pair 📖	mathematical	—	Cospherical Set Set.instInsert Set.instSingletonSet	—	RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat dist_comm dist_midpoint_left dist_midpoint_right
cospherical_singleton 📖	mathematical	—	Cospherical Set Set.instSingletonSet	—	dist_self
dist_center_eq_dist_center_of_mem_sphere 📖	mathematical	Sphere instMembershipSphere	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center	—	mem_sphere
dist_center_eq_dist_center_of_mem_sphere' 📖	mathematical	Sphere instMembershipSphere	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center	—	mem_sphere'
dist_of_mem_subset_mk_sphere 📖	mathematical	Set Set.instMembership Set.instHasSubset Metric.sphere MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	dist_of_mem_subset_sphere
dist_of_mem_subset_sphere 📖	mathematical	Set Set.instMembership Set.instHasSubset Metric.sphere MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	—	mem_sphere Sphere.mem_coe Set.mem_of_mem_of_subset
eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two 📖	—	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 Sphere instMembershipSphere	—	—	eq_of_dist_eq_of_dist_eq_of_finrank_eq_two Sphere.center_ne_iff_ne_of_mem
eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two 📖	—	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 Real.semiring Submodule.addCommMonoid Submodule.module AffineSubspace AffineSubspace.instSetLike Sphere.center Sphere instMembershipSphere	—	—	eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two Sphere.center_ne_iff_ne_of_mem
inner_nonneg_of_dist_le_radius 📖	mathematical	Sphere instMembershipSphere Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	Real Real.instLE Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Sphere.center	—	inner_pos_or_eq_of_dist_le_radius LT.lt.le vsub_self inner_zero_left instReflLe
inner_pos_of_dist_lt_radius 📖	mathematical	Sphere instMembershipSphere Real Real.instLT Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	Real Real.instLT Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Sphere.center	—	LT.lt.ne mem_sphere inner_pos_or_eq_of_dist_le_radius LT.lt.le
inner_pos_or_eq_of_dist_le_radius 📖	mathematical	Sphere instMembershipSphere Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	Real Real.instLT Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Sphere.center	—	vsub_sub_vsub_cancel_right inner_sub_left real_inner_self_eq_norm_mul_norm 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 lt_of_le_of_ne LE.le.trans real_inner_le_norm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_eq_norm_vsub mem_sphere norm_nonneg LE.le.lt_or_eq LT.lt.ne LE.le.trans_lt mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff vsub_ne_zero LE.le.not_gt dist_nonneg dist_self inner_eq_norm_mul_iff_real sub_eq_zero smul_sub smul_ne_zero_iff instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero norm_ne_zero_iff vsub_self norm_zero
inner_vsub_center_vsub_pos 📖	mathematical	Sphere instMembershipSphere	Real Real.instLT Real.instZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Sphere.center	—	dist_eq_norm_vsub' mem_sphere' Nat.instAtLeastTwoHAddOfNat vsub_add_vsub_cancel norm_add_sq_real lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_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.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo 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.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf 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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.le_of_eq_of_le neg_eq_zero sub_eq_zero_of_eq inner_neg_right neg_vsub_eq_vsub_rev Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_neg_of_lt sq_pos_of_pos IsStrictOrderedRing.toPosMulStrictMono norm_pos_iff vsub_ne_zero
inner_vsub_vsub_of_mem_sphere_of_mem_sphere 📖	mathematical	Sphere instMembershipSphere	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Sphere.center Real.instZero	—	inner_vsub_vsub_of_dist_eq_of_dist_eq dist_center_eq_dist_center_of_mem_sphere
instNonemptySphere 📖	mathematical	—	Sphere	—	—
mem_sphere 📖	mathematical	—	Sphere instMembershipSphere Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	—	—
mem_sphere' 📖	mathematical	—	Sphere instMembershipSphere Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius	—	Metric.mem_sphere'
sbtw_of_collinear_of_dist_center_lt_radius 📖	mathematical	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet Sphere instMembershipSphere Real.instLT Dist.dist PseudoMetricSpace.toDist Sphere.center Sphere.radius	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Collinear.sbtw_of_dist_eq_of_dist_lt UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace
subset_sphere 📖	mathematical	—	Set Set.instHasSubset Metric.sphere MetricSpace.toPseudoMetricSpace Sphere.center Sphere.radius Sphere instMembershipSphere	—	—
wbtw_of_collinear_of_dist_center_le_radius 📖	mathematical	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet Sphere instMembershipSphere Real.instLE Dist.dist PseudoMetricSpace.toDist Sphere.center Sphere.radius	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Collinear.wbtw_of_dist_eq_of_dist_le UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace

EuclideanGeometry.Concyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Coplanar 📖	mathematical	EuclideanGeometry.Concyclic	Coplanar Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	—
Cospherical 📖	mathematical	EuclideanGeometry.Concyclic	EuclideanGeometry.Cospherical	—	—
subset 📖	mathematical	Set Set.instHasSubset EuclideanGeometry.Concyclic	EuclideanGeometry.Concyclic	—	EuclideanGeometry.Cospherical.subset Cospherical Coplanar.subset Coplanar

EuclideanGeometry.Cospherical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineIndependent 📖	mathematical	EuclideanGeometry.Cospherical Set Set.instHasSubset Set.range	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	affineIndependent_iff_not_collinear collinear_iff_of_mem Set.mem_range_self smul_zero zero_vadd Set.forall_mem_range Set.mem_of_mem_of_subset smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero vadd_vsub vsub_eq_zero_iff_eq Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.dist_smul_vadd_eq_dist zero_smul neg_mul inner_self_eq_norm_sq_to_K
affineIndependent_of_mem_of_ne 📖	mathematical	EuclideanGeometry.Cospherical Set Set.instMembership	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Matrix.vecCons Matrix.vecEmpty	—	affineIndependent Matrix.range_cons Matrix.range_empty Set.union_empty Set.union_singleton Set.union_insert Fin.cons_injective_iff Matrix.cons_val_fin_one
affineIndependent_of_ne 📖	mathematical	EuclideanGeometry.Cospherical Set Set.instInsert Set.instSingletonSet	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Matrix.vecCons Matrix.vecEmpty	—	affineIndependent_of_mem_of_ne Set.mem_insert Set.mem_insert_of_mem Set.mem_singleton
inclusion 📖	mathematical	EuclideanGeometry.Cospherical AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Subtype.metricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder	EuclideanGeometry.Cospherical AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Subtype.metricSpace Set.image DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion	—	Isometry.cospherical Nonempty.map AffineIsometry.isometry IsScalarTower.left
inclusion_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	EuclideanGeometry.Cospherical AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Subtype.metricSpace Set.image DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion	—	Nonempty.map subtype_val_iff Set.image_image Set.image_congr
subset 📖	mathematical	Set Set.instHasSubset EuclideanGeometry.Cospherical	EuclideanGeometry.Cospherical	—	—
subtype_val 📖	mathematical	EuclideanGeometry.Cospherical AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Subtype.metricSpace	EuclideanGeometry.Cospherical Set.image AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	—	Isometry.cospherical IsScalarTower.left AffineIsometry.isometry
subtype_val_iff 📖	mathematical	—	EuclideanGeometry.Cospherical Set.image AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Subtype.metricSpace	—	Set.eq_empty_or_nonempty EuclideanGeometry.cospherical_empty EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq subtype_val

EuclideanGeometry.Sphere

Definitions

Name	Category	Theorems
IsDiameter 📖	CompData	12 math math: isDiameter_iff_right_mem_and_midpoint_eq_center, isDiameter_iff_right_mem_and_pointReflection_center_right, isDiameter_ofDiameter, IsDiameter.symm, isDiameter_comm, isDiameter_of_angle_eq_pi_div_two, isDiameter_iff_mem_and_mem_and_dist, isDiameter_iff_ofDiameter_eq, isDiameter_iff_mem_and_mem_and_wbtw, Affine.Simplex.isDiameter_ninePointCircle, isDiameter_iff_left_mem_and_midpoint_eq_center, isDiameter_iff_left_mem_and_pointReflection_center_left
center 📖	CompOp	114 math math: vadd_mem_inter_orthRadius_iff_norm_sq, EuclideanGeometry.subset_sphere, isExtTangent_iff_dist_center, isDiameter_iff_right_mem_and_midpoint_eq_center, inter_orthRadius_eq_of_dist_le_radius, secondInter_dist, IsExtTangent.dist_center, mem_orthRadius_iff_inner_right, mem_commonExtTangents_iff, isDiameter_iff_right_mem_and_pointReflection_center_right, inner_vsub_center_midpoint_vsub, Affine.Simplex.circumsphere_center, nonempty_iff, IsTangentAt.angle_eq_pi_div_two, IsDiameter.wbtw, oangle_eq_pi_sub_two_zsmul_oangle_center_left, EuclideanGeometry.dist_of_mem_subset_sphere, IsExtTangentAt.wbtw, Affine.Simplex.ninePointCircle_restrict, orthRadius_center, coe_secondInter, power_pos_iff_radius_lt_dist_center, isTangent_iff_isTangentAt_orthogonalProjection, mk_center_radius, inter_orthRadius_eq_empty_of_finrank_eq_one, tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, IsTangentAt.inner_right_eq_zero_of_mem, IsDiameter.pointReflection_center_left, IsTangentAt.radius_lt_dist_center, ncard_inter_orthRadius_eq_two_of_dist_lt_radius, orthogonalProjection_orthRadius_center, EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, dist_center_lt_radius_of_sbtw, dist_sq_eq_iff_mem_orthRadius, IsTangentAt.inner_left_eq_zero_of_mem, abs_oangle_center_left_toReal_lt_pi_div_two, Affine.Simplex.circumsphere_unique_dist_eq, EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere', dist_div_cos_oangle_center_div_two_eq_radius, power_neg_iff_dist_center_lt_radius, isExtTangentAt_center_iff, inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, abs_oangle_center_right_toReal_lt_pi_div_two, ncard_inter_orthRadius_le_two, mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq, dist_sq_eq_of_mem_orthRadius, dist_center_midpoint_lt_radius, cospherical, direction_orthRadius_le_iff, IsDiameter.sbtw, IsTangent.infDist_eq_radius, IsIntTangentAt.wbtw, dist_div_cos_oangle_center_eq_two_mul_radius, dist_orthogonalProjection_eq_radius_iff_isTangent, EuclideanGeometry.mem_sphere, IsTangent.eq_orthRadius_or_eq_orthRadius_pointReflection_of_parallel_orthRadius, IsDiameter.pointReflection_center_right, inter_orthRadius_eq_singleton_iff, power_nonneg_iff_radius_le_dist_center, Affine.Simplex.ninePointCircle_center_mem_affineSpan, oangle_eq_pi_sub_two_zsmul_oangle_center_right, power_nonpos_iff_dist_center_le_radius, EuclideanGeometry.mem_sphere', mem_coe, center_mem_orthRadius_iff, Affine.Simplex.midpoint_faceOppositeCentroid_eulerPoint, IsTangentAt.eq_orthogonalProjection, IsDiameter.midpoint_eq_center, EuclideanGeometry.inner_nonneg_of_dist_le_radius, isDiameter_iff_mem_and_mem_and_wbtw, inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one, coe_mk, inter_orthRadius_eq_empty_of_radius_lt_dist, IsTangent.isTangentAt, two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, orthRadius_le_orthRadius_iff, IsTangentAt.dist_sq_eq_of_mem, mem_inter_orthRadius_iff_vsub_mem_and_norm_sq, isIntTangentAt_center_iff, inter_orthRadius_eq_empty_iff, oangle_center_eq_two_zsmul_oangle, isTangentAt_center_iff, isIntTangent_iff_dist_center, Affine.Simplex.exsphere_center, IsTangentAt_iff_angle_eq_pi_div_two, mem_coe', inter_orthRadius_eq_singleton_of_dist_eq_radius, mem_commonIntTangents_iff, Affine.Simplex.ninePointCircle_map, center_mem_iff, mk_center, direction_orthRadius, EuclideanGeometry.inner_pos_of_dist_lt_radius, EuclideanGeometry.existsUnique_dist_eq_of_insert, AffineIndependent.existsUnique_dist_eq, IsIntTangent.dist_center, orthRadius_parallel_orthRadius_iff, EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere, Affine.Simplex.insphere_center, IsTangent.radius_le_dist_center, secondInter_eq_lineMap, secondInter_map, isDiameter_iff_left_mem_and_midpoint_eq_center, EuclideanGeometry.cospherical_iff_exists_sphere, isDiameter_iff_left_mem_and_pointReflection_center_left, EuclideanGeometry.inner_vsub_center_vsub_pos, Affine.Simplex.ninePointCircle_center, dist_orthogonalProjection_eq_radius_iff_isTangentAt, mem_orthRadius_iff_inner_left, secondInter_eq_self_iff, center_eq_iff_eq_of_mem, ext_iff, infDist_eq_radius_iff_isTangent, EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere
ofDiameter 📖	CompOp	4 math math: isDiameter_ofDiameter, isDiameter_iff_ofDiameter_eq, IsDiameter.ofDiameter_eq, angle_eq_pi_div_two_iff_mem_sphere_ofDiameter
radius 📖	CompOp	68 math math: vadd_mem_inter_orthRadius_iff_norm_sq, EuclideanGeometry.subset_sphere, isExtTangent_iff_dist_center, Affine.Simplex.insphere_radius, inter_orthRadius_eq_of_dist_le_radius, IsExtTangent.dist_center, IsDiameter.dist_left_right, Affine.Simplex.circumsphere_radius, dist_div_sin_oangle_div_two_eq_radius, Affine.Simplex.ninePointCircle_radius, nonempty_iff, EuclideanGeometry.dist_of_mem_subset_sphere, Affine.Simplex.ninePointCircle_restrict, coe_secondInter, power_pos_iff_radius_lt_dist_center, mk_center_radius, inter_orthRadius_eq_empty_of_finrank_eq_one, dist_div_sin_oangle_eq_two_mul_radius, IsDiameter.left_ne_right_iff_radius_pos, IsTangentAt.radius_lt_dist_center, ncard_inter_orthRadius_eq_two_of_dist_lt_radius, dist_center_lt_radius_of_sbtw, Affine.Simplex.circumsphere_unique_dist_eq, dist_div_cos_oangle_center_div_two_eq_radius, power_neg_iff_dist_center_lt_radius, isExtTangentAt_center_iff, ncard_inter_orthRadius_le_two, mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq, dist_center_midpoint_lt_radius, cospherical, IsTangent.infDist_eq_radius, dist_div_cos_oangle_center_eq_two_mul_radius, IsDiameter.left_eq_right_iff, mk_radius, dist_orthogonalProjection_eq_radius_iff_isTangent, EuclideanGeometry.mem_sphere, inter_orthRadius_eq_singleton_iff, power_nonneg_iff_radius_le_dist_center, power_nonpos_iff_dist_center_le_radius, EuclideanGeometry.mem_sphere', radius_nonneg_of_mem, mem_coe, isDiameter_iff_mem_and_mem_and_dist, inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one, coe_mk, inter_orthRadius_eq_empty_of_radius_lt_dist, IsTangentAt.dist_sq_eq_of_mem, mem_inter_orthRadius_iff_vsub_mem_and_norm_sq, isIntTangentAt_center_iff, inter_orthRadius_eq_empty_iff, isTangentAt_center_iff, isIntTangent_iff_dist_center, mem_coe', inter_orthRadius_eq_singleton_of_dist_eq_radius, Affine.Simplex.ninePointCircle_map, center_mem_iff, EuclideanGeometry.existsUnique_dist_eq_of_insert, AffineIndependent.existsUnique_dist_eq, IsIntTangent.dist_center, Affine.Simplex.exsphere_radius, IsTangent.radius_le_dist_center, isIntTangent_self_iff, secondInter_map, EuclideanGeometry.cospherical_iff_exists_sphere, dist_orthogonalProjection_eq_radius_iff_isTangentAt, IsDiameter.dist_left_right_div_two, ext_iff, infDist_eq_radius_iff_isTangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_iff_eq_of_mem 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	center	—	ext EuclideanGeometry.mem_sphere
center_mem_iff 📖	mathematical	—	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere center radius Real Real.instZero	—	dist_self
center_ne_iff_ne_of_mem 📖	—	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—	Iff.not center_eq_iff_eq_of_mem
coe_mk 📖	mathematical	—	Metric.sphere MetricSpace.toPseudoMetricSpace center radius	—	—
cospherical 📖	mathematical	—	EuclideanGeometry.Cospherical Metric.sphere MetricSpace.toPseudoMetricSpace center radius	—	EuclideanGeometry.cospherical_iff_exists_sphere Set.Subset.rfl
dist_center_lt_radius_of_sbtw 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Real Real.instLT Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius	—	lt_of_le_of_ne AffineMap.lineMap_apply_zero AffineMap.lineMap_apply_one dist_eq_norm_vsub EuclideanGeometry.mem_sphere vsub_left_cancel AffineMap.lineMap_same AffineMap.const_apply AffineMap.lineMap_apply vadd_vsub_assoc vsub_sub_vsub_cancel_right Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.add_eq_eval₂ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Int.cast_neg Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add 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_gt Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one dist_comm strictConvex_closedBall UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace dist_zero_right instReflLe 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 sub_add_cancel Metric.mem_ball interior_closedBall norm_eq_zero
dist_center_midpoint_lt_radius 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real Real.instLT Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center midpoint Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor radius	—	dist_center_lt_radius_of_sbtw RCLike.charZero_rclike sbtw_midpoint_of_ne Real.instIsStrictOrderedRing
ext 📖	—	center radius	—	—	—
ext_iff 📖	mathematical	—	center radius	—	ext
inner_vsub_center_midpoint_vsub 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center midpoint Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instZero	—	EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq RCLike.charZero_rclike dist_left_midpoint_eq_dist_right_midpoint EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere
isDiameter_comm 📖	mathematical	—	IsDiameter	—	IsDiameter.symm
isDiameter_iff_left_mem_and_midpoint_eq_center 📖	mathematical	—	IsDiameter EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center	—	RCLike.charZero_rclike IsDiameter.left_mem IsDiameter.midpoint_eq_center
isDiameter_iff_left_mem_and_pointReflection_center_left 📖	mathematical	—	IsDiameter EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center	—	IsDiameter.left_mem IsDiameter.pointReflection_center_left RCLike.charZero_rclike midpoint_pointReflection_right
isDiameter_iff_mem_and_mem_and_dist 📖	mathematical	—	IsDiameter InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat radius	—	Nat.instAtLeastTwoHAddOfNat IsDiameter.left_mem IsDiameter.right_mem IsDiameter.dist_left_right RCLike.charZero_rclike midpoint_eq_iff AffineEquiv.pointReflection_apply eq_vadd_iff_vsub_eq eq_of_norm_eq_of_norm_add_eq UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace EuclideanGeometry.mem_sphere' EuclideanGeometry.mem_sphere vsub_add_vsub_cancel dist_comm two_mul
isDiameter_iff_mem_and_mem_and_wbtw 📖	mathematical	—	IsDiameter InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Wbtw Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center	—	IsDiameter.left_mem IsDiameter.right_mem IsDiameter.wbtw Wbtw.dist_add_dist Nat.instAtLeastTwoHAddOfNat isDiameter_iff_mem_and_mem_and_dist two_mul EuclideanGeometry.mem_sphere' EuclideanGeometry.mem_sphere
isDiameter_iff_ofDiameter_eq 📖	mathematical	—	IsDiameter ofDiameter	—	IsDiameter.ofDiameter_eq isDiameter_ofDiameter
isDiameter_iff_right_mem_and_midpoint_eq_center 📖	mathematical	—	IsDiameter EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center	—	RCLike.charZero_rclike IsDiameter.right_mem IsDiameter.midpoint_eq_center IsDiameter.symm midpoint_comm
isDiameter_iff_right_mem_and_pointReflection_center_right 📖	mathematical	—	IsDiameter EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center	—	isDiameter_comm isDiameter_iff_left_mem_and_pointReflection_center_left
isDiameter_ofDiameter 📖	mathematical	—	IsDiameter ofDiameter	—	RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat dist_left_midpoint Real.norm_ofNat inv_mul_eq_div
mem_coe 📖	mathematical	—	Set Set.instMembership Metric.sphere MetricSpace.toPseudoMetricSpace center radius EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
mem_coe' 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
mk_center 📖	mathematical	—	center	—	—
mk_center_radius 📖	mathematical	—	center radius	—	ext
mk_radius 📖	mathematical	—	radius	—	—
ne_iff 📖	—	—	—	—	not_and_or ext_iff
nonempty_iff 📖	mathematical	—	Set.Nonempty Metric.sphere MetricSpace.toPseudoMetricSpace center radius Real Real.instLE Real.instZero	—	radius_nonneg_of_mem NormedSpace.sphere_nonempty EMetric.instNontrivialTopologyOfNontrivial dist_vadd_left sub_zero
radius_nonneg_of_mem 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	Real Real.instLE Real.instZero radius	—	Metric.nonneg_of_mem_sphere

EuclideanGeometry.Sphere.IsDiameter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_left_right 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.Sphere.radius	—	Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.mem_sphere left_mem RCLike.charZero_rclike midpoint_eq_center dist_left_midpoint Real.norm_ofNat mul_inv_cancel_left₀
dist_left_right_div_two 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	Real DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.Sphere.radius	—	Nat.instAtLeastTwoHAddOfNat dist_left_right mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass RCLike.charZero_rclike
left_eq_of_isDiameter 📖	—	EuclideanGeometry.Sphere.IsDiameter	—	—	pointReflection_center_right
left_eq_right_iff 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	EuclideanGeometry.Sphere.radius Real Real.instZero	—	dist_eq_zero Nat.instAtLeastTwoHAddOfNat dist_left_right NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike
left_mem 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
left_ne_right_iff_radius_ne_zero 📖	—	EuclideanGeometry.Sphere.IsDiameter	—	—	Iff.not left_eq_right_iff
left_ne_right_iff_radius_pos 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	Real Real.instLT Real.instZero EuclideanGeometry.Sphere.radius	—	left_ne_right_iff_radius_ne_zero lt_iff_le_and_ne EuclideanGeometry.Sphere.radius_nonneg_of_mem left_mem
midpoint_eq_center 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	—
ofDiameter_eq 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	EuclideanGeometry.Sphere.ofDiameter	—	EuclideanGeometry.Sphere.ext RCLike.charZero_rclike midpoint_eq_center Nat.instAtLeastTwoHAddOfNat dist_left_right_div_two
pointReflection_center_left 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	RCLike.charZero_rclike midpoint_eq_center Equiv.pointReflection_midpoint_left
pointReflection_center_right 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	RCLike.charZero_rclike midpoint_eq_center Equiv.pointReflection_midpoint_right
right_eq_of_isDiameter 📖	—	EuclideanGeometry.Sphere.IsDiameter	—	—	pointReflection_center_left
right_mem 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	EuclideanGeometry.mem_sphere left_mem RCLike.charZero_rclike midpoint_eq_center dist_left_midpoint_eq_dist_right_midpoint
sbtw 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	RCLike.charZero_rclike midpoint_eq_center sbtw_midpoint_of_ne Real.instIsStrictOrderedRing left_ne_right_iff_radius_ne_zero
wbtw 📖	mathematical	EuclideanGeometry.Sphere.IsDiameter	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	RCLike.charZero_rclike midpoint_eq_center wbtw_midpoint Real.instIsStrictOrderedRing

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cospherical 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace EuclideanGeometry.Cospherical	EuclideanGeometry.Cospherical Set.image	—	dist_eq

---

← Back to Index