Tangent

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

Statistics

Metric	Count
Definitions IsExtTangent, IsExtTangentAt, IsIntTangent, IsIntTangentAt, IsTangent, IsTangentAt, commonExtTangents, commonIntTangents, commonTangents, tangentSet, tangentsFrom	11
Theorems dist_center, isExtTangent, mem_left, mem_right, wbtw, dist_center, isIntTangent, mem_left, mem_right, wbtw, eq_orthRadius_or_eq_orthRadius_pointReflection_of_parallel_orthRadius, infDist_eq_radius, isTangentAt, notMem_of_dist_lt, radius_le_dist_center, dist_eq_of_mem_of_mem, dist_sq_eq_of_mem, eq_of_isTangentAt, eq_of_mem_of_mem, eq_orthRadius_of_finrank_add_one_eq, eq_orthogonalProjection, inner_left_eq_zero_of_mem, inner_right_eq_zero_of_mem, isTangent, le_orthRadius, mem_and_mem_iff_eq, mem_space, mem_sphere, radius_lt_dist_center, commonIntTangents_union_commonExtTangents, commonTangents_comm, dist_orthogonalProjection_eq_radius_iff_isTangent, dist_orthogonalProjection_eq_radius_iff_isTangentAt, infDist_eq_radius_iff_isTangent, isExtTangentAt_center_iff, isExtTangentAt_comm, isExtTangent_comm, isExtTangent_iff_dist_center, isIntTangentAt_center_iff, isIntTangentAt_self_iff_mem, isIntTangent_iff_dist_center, isIntTangent_self_iff, isTangentAt_center_iff, isTangentAt_orthRadius_iff_mem, isTangent_iff_isTangentAt_orthogonalProjection, isTangent_of_mem_tangentSet, isTangent_of_mem_tangentsFrom, isTangent_orthRadius_iff_mem, mem_commonExtTangents_iff, mem_commonIntTangents_iff, mem_commonTangents_iff, mem_of_mem_tangentsFrom, mem_tangentSet_iff, mem_tangentSet_of_mem_tangentsFrom, mem_tangentsFrom_iff	55
Total	66

EuclideanGeometry.Sphere

Definitions

Name	Category	Theorems
IsExtTangent 📖	MathDef	3 math math: isExtTangent_iff_dist_center, isExtTangent_comm, IsExtTangentAt.isExtTangent
IsExtTangentAt 📖	CompData	2 math math: isExtTangentAt_center_iff, isExtTangentAt_comm
IsIntTangent 📖	MathDef	3 math math: IsIntTangentAt.isIntTangent, isIntTangent_iff_dist_center, isIntTangent_self_iff
IsIntTangentAt 📖	CompData	2 math math: isIntTangentAt_self_iff_mem, isIntTangentAt_center_iff
IsTangent 📖	MathDef	7 math math: isTangent_of_mem_tangentSet, isTangent_orthRadius_iff_mem, isTangent_iff_isTangentAt_orthogonalProjection, isTangent_of_mem_tangentsFrom, dist_orthogonalProjection_eq_radius_iff_isTangent, IsTangentAt.isTangent, infDist_eq_radius_iff_isTangent
IsTangentAt 📖	CompData	13 math math: Affine.Simplex.isTangentAt_insphere_iff_eq_touchpoint, isTangentAt_of_dist_sq_eq_power, isTangentAt_orthRadius_iff_mem, Affine.Simplex.isTangentAt_insphere_touchpoint, isTangent_iff_isTangentAt_orthogonalProjection, Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, IsTangentAt_of_angle_eq_pi_div_two, Affine.Simplex.ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, IsTangent.isTangentAt, isTangentAt_center_iff, IsTangentAt_iff_angle_eq_pi_div_two, isTangentAt_iff_dist_sq_eq_power, dist_orthogonalProjection_eq_radius_iff_isTangentAt
commonExtTangents 📖	CompOp	2 math math: mem_commonExtTangents_iff, commonIntTangents_union_commonExtTangents
commonIntTangents 📖	CompOp	2 math math: commonIntTangents_union_commonExtTangents, mem_commonIntTangents_iff
commonTangents 📖	CompOp	5 math math: mem_commonExtTangents_iff, mem_commonTangents_iff, commonTangents_comm, commonIntTangents_union_commonExtTangents, mem_commonIntTangents_iff
tangentSet 📖	CompOp	4 math math: mem_tangentsFrom_iff, mem_commonTangents_iff, mem_tangentSet_of_mem_tangentsFrom, mem_tangentSet_iff
tangentsFrom 📖	CompOp	1 math math: mem_tangentsFrom_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commonIntTangents_union_commonExtTangents 📖	mathematical	—	Set AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.instUnion commonIntTangents commonExtTangents commonTangents	—	Set.ext Set.mem_union mem_commonIntTangents_iff mem_commonExtTangents_iff Sbtw.wbtw Mathlib.Tactic.Push.not_and_eq
commonTangents_comm 📖	mathematical	—	commonTangents	—	Set.inter_comm
dist_orthogonalProjection_eq_radius_iff_isTangent 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center AffineSubspace Real NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike EuclideanGeometry.orthogonalProjection radius IsTangent	—	IsTangentAt.isTangent dist_orthogonalProjection_eq_radius_iff_isTangentAt EuclideanGeometry.dist_orthogonalProjection_eq_infDist IsTangent.infDist_eq_radius
dist_orthogonalProjection_eq_radius_iff_isTangentAt 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center AffineSubspace Real NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike EuclideanGeometry.orthogonalProjection radius IsTangentAt	—	EuclideanGeometry.mem_sphere' EuclideanGeometry.orthogonalProjection_mem mem_orthRadius_iff_inner_left EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal EuclideanGeometry.vsub_orthogonalProjection_mem_direction EuclideanGeometry.dist_orthogonalProjection_eq_infDist IsTangent.infDist_eq_radius IsTangentAt.isTangent
infDist_eq_radius_iff_isTangent 📖	mathematical	—	Metric.infDist MetricSpace.toPseudoMetricSpace center SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike radius IsTangent	—	EuclideanGeometry.dist_orthogonalProjection_eq_infDist dist_orthogonalProjection_eq_radius_iff_isTangent
isExtTangentAt_center_iff 📖	mathematical	—	IsExtTangentAt center radius Real Real.instZero EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	center_mem_iff Real.instIsOrderedRing
isExtTangentAt_comm 📖	mathematical	—	IsExtTangentAt	—	IsExtTangentAt.symm
isExtTangent_comm 📖	mathematical	—	IsExtTangent	—	IsExtTangent.symm
isExtTangent_iff_dist_center 📖	mathematical	—	IsExtTangent Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center Real Real.instAdd radius Real.instLE Real.instZero	—	IsExtTangent.dist_center radius_nonneg_of_mem div_zero AffineMap.lineMap_apply_zero Mathlib.Tactic.Linarith.eq_of_not_lt_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.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf 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_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.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Linarith.le_of_le_of_eq sub_eq_zero_of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.le_of_eq_of_le neg_eq_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf dist_lineMap_left norm_div abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_nonneg Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial dist_lineMap_right one_sub_div add_sub_cancel_left abs_div Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_ne' div_le_one le_of_not_gt
isIntTangentAt_center_iff 📖	mathematical	—	IsIntTangentAt center radius Real Real.instZero EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	center_mem_iff Real.instIsOrderedRing
isIntTangentAt_self_iff_mem 📖	mathematical	—	IsIntTangentAt EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	Real.instIsOrderedRing
isIntTangent_iff_dist_center 📖	mathematical	—	IsIntTangent Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center Real Real.instSub radius Real.instLE Real.instZero	—	IsIntTangent.dist_center radius_nonneg_of_mem ext sub_eq_zero dist_self abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_comm dist_nonneg dist_eq_zero dist_lineMap_right one_sub_div sub_sub_cancel_left abs_div Real.instIsStrictOrderedRing abs_neg Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf dist_lineMap_left norm_div wbtw_iff_left_eq_or_right_mem_image_Ici Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors one_le_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl 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.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_gt Mathlib.Tactic.Ring.add_pf_add_zero 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.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt
isIntTangent_self_iff 📖	mathematical	—	IsIntTangent Real Real.instLE Real.instZero radius	—	nonempty_iff
isTangentAt_center_iff 📖	mathematical	—	IsTangentAt center radius Real Real.instZero AffineSubspace Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	—	center_mem_iff orthRadius_center
isTangentAt_orthRadius_iff_mem 📖	mathematical	—	IsTangentAt orthRadius EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	IsTangentAt.mem_sphere self_mem_orthRadius le_rfl
isTangent_iff_isTangentAt_orthogonalProjection 📖	mathematical	—	IsTangent IsTangentAt 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 DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike EuclideanGeometry.orthogonalProjection center	—	dist_orthogonalProjection_eq_radius_iff_isTangent dist_orthogonalProjection_eq_radius_iff_isTangentAt
isTangent_of_mem_tangentSet 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership tangentSet	IsTangent	—	isTangent_orthRadius_iff_mem
isTangent_of_mem_tangentsFrom 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership tangentsFrom	IsTangent	—	isTangent_of_mem_tangentSet
isTangent_orthRadius_iff_mem 📖	mathematical	—	IsTangent orthRadius EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	orthRadius_le_orthRadius_iff center_mem_orthRadius_iff IsTangentAt.isTangent isTangentAt_orthRadius_iff_mem
mem_commonExtTangents_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership commonExtTangents commonTangents Sbtw Real.partialOrder center	—	—
mem_commonIntTangents_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership commonIntTangents commonTangents SetLike.instMembership AffineSubspace.instSetLike Wbtw Real.partialOrder center	—	—
mem_commonTangents_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership commonTangents tangentSet	—	—
mem_of_mem_tangentsFrom 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership tangentsFrom	SetLike.instMembership AffineSubspace.instSetLike	—	—
mem_tangentSet_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership tangentSet EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere orthRadius	—	—
mem_tangentSet_of_mem_tangentsFrom 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership tangentsFrom	tangentSet	—	—
mem_tangentsFrom_iff 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instMembership tangentsFrom tangentSet SetLike.instMembership AffineSubspace.instSetLike	—	—

EuclideanGeometry.Sphere.IsExtTangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_center 📖	mathematical	EuclideanGeometry.Sphere.IsExtTangent	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center Real Real.instAdd EuclideanGeometry.Sphere.radius	—	dist_add_dist_eq_iff UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace EuclideanGeometry.mem_sphere'

EuclideanGeometry.Sphere.IsExtTangentAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isExtTangent 📖	mathematical	EuclideanGeometry.Sphere.IsExtTangentAt	EuclideanGeometry.Sphere.IsExtTangent	—	—
mem_left 📖	mathematical	EuclideanGeometry.Sphere.IsExtTangentAt	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
mem_right 📖	mathematical	EuclideanGeometry.Sphere.IsExtTangentAt	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
wbtw 📖	mathematical	EuclideanGeometry.Sphere.IsExtTangentAt	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	—

EuclideanGeometry.Sphere.IsIntTangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_center 📖	mathematical	EuclideanGeometry.Sphere.IsIntTangent	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center Real Real.instSub EuclideanGeometry.Sphere.radius	—	EuclideanGeometry.mem_sphere' dist_add_dist_eq_iff UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace dist_comm add_sub_cancel_right

EuclideanGeometry.Sphere.IsIntTangentAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntTangent 📖	mathematical	EuclideanGeometry.Sphere.IsIntTangentAt	EuclideanGeometry.Sphere.IsIntTangent	—	—
mem_left 📖	mathematical	EuclideanGeometry.Sphere.IsIntTangentAt	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
mem_right 📖	mathematical	EuclideanGeometry.Sphere.IsIntTangentAt	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
wbtw 📖	mathematical	EuclideanGeometry.Sphere.IsIntTangentAt	Wbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center	—	—

EuclideanGeometry.Sphere.IsTangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_orthRadius_or_eq_orthRadius_pointReflection_of_parallel_orthRadius 📖	mathematical	EuclideanGeometry.Sphere.IsTangent AffineSubspace.Parallel Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.orthRadius EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.pointReflection SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup EuclideanGeometry.Sphere.center	—	AffineSubspace.direction_le EuclideanGeometry.Sphere.direction_orthRadius_le_iff AffineSubspace.Parallel.direction_eq eq_or_ne dist_eq_zero EuclideanGeometry.mem_sphere EuclideanGeometry.Sphere.orthRadius_center AffineSubspace.eq_of_direction_eq_of_nonempty_of_le zero_smul eq_or_eq_neg_of_abs_eq right_eq_mul₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain norm_smul NormedSpace.toNormSMulClass one_smul eq_vadd_iff_vsub_eq neg_smul neg_vsub_eq_vsub_rev EuclideanGeometry.Sphere.direction_orthRadius vsub_self Submodule.span_zero_singleton Submodule.span_singleton_smul_eq Ne.isUnit
infDist_eq_radius 📖	mathematical	EuclideanGeometry.Sphere.IsTangent	Metric.infDist MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace.instSetLike EuclideanGeometry.Sphere.radius	—	le_antisymm EuclideanGeometry.mem_sphere' EuclideanGeometry.Sphere.IsTangentAt.mem_sphere Metric.infDist_le_dist_of_mem EuclideanGeometry.Sphere.IsTangentAt.mem_space Metric.infDist_eq_iInf le_ciInf dist_comm radius_le_dist_center EuclideanGeometry.Sphere.IsTangentAt.isTangent
isTangentAt 📖	mathematical	EuclideanGeometry.Sphere.IsTangent	EuclideanGeometry.Sphere.IsTangentAt 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 DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike EuclideanGeometry.orthogonalProjection EuclideanGeometry.Sphere.center	—	EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection
notMem_of_dist_lt 📖	mathematical	EuclideanGeometry.Sphere.IsTangent Real Real.instLT Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace EuclideanGeometry.Sphere.center EuclideanGeometry.Sphere.radius	AffineSubspace Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike	—	Mathlib.Tactic.Contrapose.contrapose₃ radius_le_dist_center
radius_le_dist_center 📖	mathematical	EuclideanGeometry.Sphere.IsTangent AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Real.instLE EuclideanGeometry.Sphere.radius Dist.dist PseudoMetricSpace.toDist EuclideanGeometry.Sphere.center	—	le_of_sq_le_sq Real.instIsStrictOrderedRing EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem le_add_iff_nonneg_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_nonneg

EuclideanGeometry.Sphere.IsTangentAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_eq_of_mem_of_mem 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Dist.dist PseudoMetricSpace.toDist	—	dist_sq_eq_of_mem sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_nonneg add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd
dist_sq_eq_of_mem 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist EuclideanGeometry.Sphere.center Real.instAdd EuclideanGeometry.Sphere.radius	—	mem_sphere 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 inner_left_eq_zero_of_mem
eq_of_isTangentAt 📖	—	EuclideanGeometry.Sphere.IsTangentAt	—	—	inner_left_eq_zero_of_mem mem_space inner_self_eq_norm_sq_to_K isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat vsub_sub_vsub_cancel_right inner_sub_right sub_eq_zero neg_eq_zero inner_neg_left neg_vsub_eq_vsub_rev
eq_of_mem_of_mem 📖	—	EuclideanGeometry.Sphere.IsTangentAt EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	—	—	mem_and_mem_iff_eq
eq_orthRadius_of_finrank_add_one_eq 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt 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 ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	EuclideanGeometry.Sphere.orthRadius	—	Module.finite_of_finrank_eq_succ commRing_strongRankCondition Real.instNontrivial Module.Free.of_divisionRing Iff.not EuclideanGeometry.Sphere.center_mem_iff mem_sphere AffineSubspace.eq_of_direction_eq_of_nonempty_of_le Submodule.eq_of_le_of_finrank_eq FiniteDimensional.finiteDimensional_submodule AffineSubspace.direction_le le_orthRadius EuclideanGeometry.Sphere.finrank_orthRadius mem_space
eq_orthogonalProjection 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt	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 DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike EuclideanGeometry.orthogonalProjection EuclideanGeometry.Sphere.center	—	eq_of_isTangentAt isTangent EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection
inner_left_eq_zero_of_mem 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup EuclideanGeometry.Sphere.center Real.instZero	—	EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left le_orthRadius
inner_right_eq_zero_of_mem 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup EuclideanGeometry.Sphere.center Real.instZero	—	EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right le_orthRadius
isTangent 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt	EuclideanGeometry.Sphere.IsTangent	—	—
le_orthRadius 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt	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.Sphere.orthRadius	—	—
mem_and_mem_iff_eq 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	—	dist_sq_eq_of_mem AddLeftCancelSemigroup.toIsLeftCancelAdd isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat mem_sphere mem_space
mem_space 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	—	—
mem_sphere 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere	—	—
radius_lt_dist_center 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Real.instLT EuclideanGeometry.Sphere.radius Dist.dist PseudoMetricSpace.toDist EuclideanGeometry.Sphere.center	—	dist_sq_eq_of_mem IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing abs_of_nonneg EuclideanGeometry.Sphere.radius_nonneg_of_mem mem_sphere abs_dist

---

← Back to Index