Circumcenter

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

Statistics

Metric	Count
Definitions PointsWithCircumcenterIndex, centroidWeightsWithCircumcenter, circumcenter, circumcenterWeightsWithCircumcenter, circumradius, circumsphere, instFintypePointsWithCircumcenterIndex, pointIndexEmbedding, pointWeightsWithCircumcenter, pointsWithCircumcenter, pointsWithCircumcenterIndexInhabited, reflectionCircumcenterWeightsWithCircumcenter	12
Theorems centroid_eq_affineCombination_of_pointsWithCircumcenter, circumcenter_eq_affineCombination_of_pointsWithCircumcenter, circumcenter_eq_centroid, circumcenter_eq_of_range_eq, circumcenter_eq_point, circumcenter_map, circumcenter_mem_affineSpan, circumcenter_ne_point, circumcenter_reindex, circumcenter_restrict, circumradius_map, circumradius_nonneg, circumradius_pos, circumradius_reindex, circumradius_restrict, circumsphere_center, circumsphere_radius, circumsphere_reindex, circumsphere_unique_dist_eq, dist_circumcenter_eq_circumradius, dist_circumcenter_eq_circumradius', dist_circumcenter_sq_eq_sq_sub_circumradius, eq_circumcenter_of_dist_eq, eq_circumradius_of_dist_eq, mem_circumsphere, orthogonalProjection_circumcenter, orthogonalProjection_eq_circumcenter_of_dist_eq, orthogonalProjection_eq_circumcenter_of_exists_dist_eq, point_eq_affineCombination_of_pointsWithCircumcenter, pointsWithCircumcenter_eq_circumcenter, pointsWithCircumcenter_point, reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, sum_centroidWeightsWithCircumcenter, sum_circumcenterWeightsWithCircumcenter, sum_pointWeightsWithCircumcenter, sum_pointsWithCircumcenter, sum_reflectionCircumcenterWeightsWithCircumcenter, existsUnique_dist_eq, circumcenter_eq_of_cospherical, circumcenter_eq_of_cospherical_subset, circumradius_eq_of_cospherical, circumradius_eq_of_cospherical_subset, circumsphere_eq_of_cospherical, circumsphere_eq_of_cospherical_subset, cospherical_iff_exists_mem_of_complete, cospherical_iff_exists_mem_of_finiteDimensional, eq_or_eq_reflection_of_dist_eq, existsUnique_dist_eq_of_insert, exists_circumcenter_eq_of_cospherical, exists_circumcenter_eq_of_cospherical_subset, exists_circumradius_eq_of_cospherical, exists_circumradius_eq_of_cospherical_subset, exists_circumsphere_eq_of_cospherical, exists_circumsphere_eq_of_cospherical_subset	54
Total	66

Affine.Simplex

Definitions

Name	Category	Theorems
PointsWithCircumcenterIndex 📖	CompData	14 math math: mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, sum_mongePointWeightsWithCircumcenter, circumcenter_eq_affineCombination_of_pointsWithCircumcenter, sum_mongePointVSubFaceCentroidWeightsWithCircumcenter, mongePoint_eq_affineCombination_of_pointsWithCircumcenter, sum_circumcenterWeightsWithCircumcenter, sum_reflectionCircumcenterWeightsWithCircumcenter, point_eq_affineCombination_of_pointsWithCircumcenter, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, sum_pointWeightsWithCircumcenter, sum_pointsWithCircumcenter, reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, centroid_eq_affineCombination_of_pointsWithCircumcenter, sum_centroidWeightsWithCircumcenter
centroidWeightsWithCircumcenter 📖	CompOp	3 math math: mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, centroid_eq_affineCombination_of_pointsWithCircumcenter, sum_centroidWeightsWithCircumcenter
circumcenter 📖	CompOp	31 math math: smul_mongePoint_vsub_circumcenter_eq_sum_vsub, circumcenter_map, circumcenter_mem_affineSpan, Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter, circumsphere_center, circumcenter_reindex, circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Affine.Triangle.dist_circumcenter_reflection_orthocenter, circumcenter_eq_point, pointsWithCircumcenter_eq_circumcenter, Affine.Triangle.dist_orthocenter_reflection_circumcenter, EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset, orthogonalProjection_circumcenter, orthogonalProjection_eq_circumcenter_of_exists_dist_eq, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, circumcenter_restrict, dist_circumcenter_eq_circumradius, dist_circumcenter_eq_circumradius', mongePoint_eq_smul_vsub_vadd_circumcenter, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, orthogonalProjection_eq_circumcenter_of_dist_eq, EuclideanGeometry.circumcenter_eq_of_cospherical_subset, EuclideanGeometry.circumcenter_eq_of_cospherical, circumcenter_eq_of_range_eq, reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Affine.Triangle.orthocenter_vsub_circumcenter_eq_sum_vsub, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, circumcenter_eq_centroid, ninePointCircle_center, EuclideanGeometry.exists_circumcenter_eq_of_cospherical, eq_circumcenter_of_dist_eq
circumcenterWeightsWithCircumcenter 📖	CompOp	2 math math: circumcenter_eq_affineCombination_of_pointsWithCircumcenter, sum_circumcenterWeightsWithCircumcenter
circumradius 📖	CompOp	25 math math: circumradius_nonneg, EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset, circumsphere_radius, dist_circumcenter_sq_eq_sq_sub_circumradius, circumradius_restrict, ninePointCircle_radius, Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius, Affine.Triangle.dist_circumcenter_reflection_orthocenter, Affine.Triangle.dist_orthocenter_reflection_circumcenter, Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius, dist_circumcenter_eq_circumradius, dist_circumcenter_eq_circumradius', EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter, EuclideanGeometry.circumradius_eq_of_cospherical_subset, circumradius_pos, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, EuclideanGeometry.circumradius_eq_of_cospherical, Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius, eq_circumradius_of_dist_eq, circumradius_reindex, Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius, EuclideanGeometry.OrthocentricSystem.exists_circumradius_eq, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, circumradius_map, EuclideanGeometry.exists_circumradius_eq_of_cospherical
circumsphere 📖	CompOp	13 math math: Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq, mem_circumsphere, circumsphere_radius, ninePointCircle_eq_circumsphere_medial, circumsphere_center, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, circumsphere_unique_dist_eq, Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq, EuclideanGeometry.exists_circumsphere_eq_of_cospherical, EuclideanGeometry.circumsphere_eq_of_cospherical, EuclideanGeometry.circumsphere_eq_of_cospherical_subset, circumsphere_reindex, EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset
instFintypePointsWithCircumcenterIndex 📖	CompOp	13 math math: sum_mongePointWeightsWithCircumcenter, circumcenter_eq_affineCombination_of_pointsWithCircumcenter, sum_mongePointVSubFaceCentroidWeightsWithCircumcenter, mongePoint_eq_affineCombination_of_pointsWithCircumcenter, sum_circumcenterWeightsWithCircumcenter, sum_reflectionCircumcenterWeightsWithCircumcenter, point_eq_affineCombination_of_pointsWithCircumcenter, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, sum_pointWeightsWithCircumcenter, sum_pointsWithCircumcenter, reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, centroid_eq_affineCombination_of_pointsWithCircumcenter, sum_centroidWeightsWithCircumcenter
pointIndexEmbedding 📖	CompOp	—
pointWeightsWithCircumcenter 📖	CompOp	2 math math: point_eq_affineCombination_of_pointsWithCircumcenter, sum_pointWeightsWithCircumcenter
pointsWithCircumcenter 📖	CompOp	8 math math: circumcenter_eq_affineCombination_of_pointsWithCircumcenter, mongePoint_eq_affineCombination_of_pointsWithCircumcenter, pointsWithCircumcenter_eq_circumcenter, pointsWithCircumcenter_point, point_eq_affineCombination_of_pointsWithCircumcenter, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, centroid_eq_affineCombination_of_pointsWithCircumcenter
pointsWithCircumcenterIndexInhabited 📖	CompOp	—
reflectionCircumcenterWeightsWithCircumcenter 📖	CompOp	2 math math: sum_reflectionCircumcenterWeightsWithCircumcenter, reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centroid_eq_affineCombination_of_pointsWithCircumcenter 📖	mathematical	—	Finset.centroid Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing DFunLike.coe AffineMap Pi.addCommGroup PointsWithCircumcenterIndex Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ instFintypePointsWithCircumcenterIndex pointsWithCircumcenter centroidWeightsWithCircumcenter	—	AddTorsor.nonempty Finset.weightedVSubOfPoint_apply sum_pointsWithCircumcenter Finset.sum_congr zero_smul add_zero Finset.sum_indicator_subset_of_eq_zero Finset.subset_univ Set.indicator_apply
circumcenter_eq_affineCombination_of_pointsWithCircumcenter 📖	mathematical	—	circumcenter DFunLike.coe AffineMap Real Real.instRing Pi.addCommGroup PointsWithCircumcenterIndex Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike Finset.affineCombination Finset.univ instFintypePointsWithCircumcenterIndex pointsWithCircumcenter circumcenterWeightsWithCircumcenter	—	pointsWithCircumcenter_eq_circumcenter Finset.affineCombination_of_eq_one_of_eq_zero Finset.mem_univ
circumcenter_eq_centroid 📖	mathematical	—	circumcenter Finset.centroid Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.univ Fin.fintype points Real.instRing	—	Nat.instAtLeastTwoHAddOfNat Finset.centroid_pair_fin RCLike.charZero_rclike dist_eq_norm_vsub vsub_vadd_eq_vsub_sub one_smul Fintype.complete vsub_self smul_zero zero_sub norm_neg Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Set.pairwise_eq_iff_exists_eq eq_circumcenter_of_dist_eq centroid_mem_affineSpan_of_card_eq_add_one Finset.card_fin Set.mem_univ
circumcenter_eq_of_range_eq 📖	mathematical	Set.range points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	circumcenter	—	circumcenter_mem_affineSpan Set.mem_range_self Set.mem_range dist_circumcenter_eq_circumradius eq_circumcenter_of_dist_eq
circumcenter_eq_point 📖	mathematical	—	circumcenter points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	circumcenter_mem_affineSpan Fin.eq_zero Set.range_unique Unique.instSubsingleton
circumcenter_map 📖	mathematical	—	circumcenter map Real Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineIsometry.toAffineMap AffineIsometry.injective DFunLike.coe AffineIsometry AffineIsometry.instFunLike	—	AffineIsometry.injective eq_circumcenter_of_dist_eq map_points Set.range_comp AffineSubspace.map_span AffineSubspace.mem_map_of_mem circumcenter_mem_affineSpan AffineIsometry.coe_toAffineMap AffineIsometry.dist_map dist_circumcenter_eq_circumradius
circumcenter_mem_affineSpan 📖	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 affineSpan Set.range points circumcenter	—	circumsphere_unique_dist_eq
circumcenter_ne_point 📖	—	—	—	—	dist_ne_zero dist_circumcenter_eq_circumradius' LT.lt.ne' circumradius_pos
circumcenter_reindex 📖	mathematical	—	circumcenter reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	circumsphere_reindex
circumcenter_restrict 📖	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 affineSpan Set.range points	SetLike.instMembership AffineSubspace.instSetLike circumcenter Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor Nonempty.map DFunLike.coe AffineMap Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange circumcenter_map
circumradius_map 📖	mathematical	—	circumradius map Real Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineIsometry.toAffineMap AffineIsometry.injective	—	AffineIsometry.injective eq_circumradius_of_dist_eq map_points Set.range_comp AffineSubspace.map_span AffineSubspace.mem_map_of_mem circumcenter_mem_affineSpan AffineIsometry.coe_toAffineMap AffineIsometry.dist_map dist_circumcenter_eq_circumradius
circumradius_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero circumradius	—	dist_nonneg dist_circumcenter_eq_circumradius
circumradius_pos 📖	mathematical	—	Real Real.instLT Real.instZero circumradius	—	lt_of_le_of_ne circumradius_nonneg dist_circumcenter_eq_circumradius AffineIndependent.injective Real.instNontrivial independent Fin.instNeZeroHAddNatOfNat_mathlib
circumradius_reindex 📖	mathematical	—	circumradius reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	circumsphere_reindex
circumradius_restrict 📖	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 affineSpan Set.range points	circumradius Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor Nonempty.map DFunLike.coe AffineMap Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange circumradius_map
circumsphere_center 📖	mathematical	—	EuclideanGeometry.Sphere.center circumsphere circumcenter	—	—
circumsphere_radius 📖	mathematical	—	EuclideanGeometry.Sphere.radius circumsphere circumradius	—	—
circumsphere_reindex 📖	mathematical	—	circumsphere reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	circumsphere_unique_dist_eq reindex_range_points
circumsphere_unique_dist_eq 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points EuclideanGeometry.Sphere.center circumsphere Set Set.instHasSubset Metric.sphere EuclideanGeometry.Sphere.radius	—	AffineIndependent.existsUnique_dist_eq Finite.of_fintype independent
dist_circumcenter_eq_circumradius 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor circumcenter circumradius	—	EuclideanGeometry.dist_of_mem_subset_sphere Set.mem_range_self circumsphere_unique_dist_eq
dist_circumcenter_eq_circumradius' 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace circumcenter points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor circumradius	—	dist_comm dist_circumcenter_eq_circumradius
dist_circumcenter_sq_eq_sq_sub_circumradius 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range 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 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan circumcenter	Real.instMul Real.instSub circumradius	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange dist_comm dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq dist_circumcenter_eq_circumradius add_sub_cancel_left
eq_circumcenter_of_dist_eq 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points Dist.dist PseudoMetricSpace.toDist	circumcenter	—	circumsphere_unique_dist_eq EuclideanGeometry.subset_sphere
eq_circumradius_of_dist_eq 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points Dist.dist PseudoMetricSpace.toDist	circumradius	—	circumsphere_unique_dist_eq EuclideanGeometry.subset_sphere
mem_circumsphere 📖	mathematical	—	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere circumsphere points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	dist_circumcenter_eq_circumradius
orthogonalProjection_circumcenter 📖	mathematical	Finset.card	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 affineSpan Set.range points face Real.instRing Real.normedField 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 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan circumcenter	—	orthogonalProjection_eq_circumcenter_of_exists_dist_eq dist_circumcenter_eq_circumradius
orthogonalProjection_eq_circumcenter_of_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range 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 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan circumcenter	—	orthogonalProjection_eq_circumcenter_of_exists_dist_eq
orthogonalProjection_eq_circumcenter_of_exists_dist_eq 📖	mathematical	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range 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 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan circumcenter	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.forall_mem_range Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Finite.of_fintype EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq subset_affineSpan eq_circumcenter_of_dist_eq EuclideanGeometry.orthogonalProjection_mem Set.mem_range_self
point_eq_affineCombination_of_pointsWithCircumcenter 📖	mathematical	—	points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace DFunLike.coe AffineMap Pi.addCommGroup PointsWithCircumcenterIndex Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ instFintypePointsWithCircumcenterIndex pointsWithCircumcenter pointWeightsWithCircumcenter	—	pointsWithCircumcenter_point Finset.affineCombination_of_eq_one_of_eq_zero Finset.mem_univ
pointsWithCircumcenter_eq_circumcenter 📖	mathematical	—	pointsWithCircumcenter PointsWithCircumcenterIndex.circumcenterIndex circumcenter	—	—
pointsWithCircumcenter_point 📖	mathematical	—	pointsWithCircumcenter PointsWithCircumcenterIndex.pointIndex points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	—
reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv Real DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike EuclideanGeometry.reflection affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor Set.image points Real.normedField Set Set.instInsert Set.instSingletonSet instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing complete_of_proper Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Real.instDivisionRing Finite.of_fintype Fin.fintype circumcenter AffineMap Pi.addCommGroup PointsWithCircumcenterIndex Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ instFintypePointsWithCircumcenterIndex pointsWithCircumcenter reflectionCircumcenterWeightsWithCircumcenter	—	Finset.card_insert_of_notMem Finset.card_singleton instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Finite.of_fintype Set.instNonemptyRange EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace range_face_points Finset.coe_insert Finset.coe_singleton EuclideanGeometry.reflection_apply' orthogonalProjection_circumcenter circumcenter_eq_centroid face_centroid_eq_centroid centroid_eq_affineCombination_of_pointsWithCircumcenter circumcenter_eq_affineCombination_of_pointsWithCircumcenter vsub_eq_zero_iff_eq Finset.affineCombination_vsub Finset.weightedVSub_vadd_affineCombination AddTorsor.nonempty Finset.weightedVSub_apply sum_pointsWithCircumcenter Finset.sum_congr sub_smul add_smul ite_smul zero_smul sub_zero apply_ite₂ add_zero zero_sub neg_smul sub_self Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_smul Finset.sum_const_zero
sum_centroidWeightsWithCircumcenter 📖	mathematical	Finset.Nonempty	Finset.sum PointsWithCircumcenterIndex Real Real.instAddCommMonoid Finset.univ instFintypePointsWithCircumcenterIndex centroidWeightsWithCircumcenter Real.instOne	—	sum_pointsWithCircumcenter Finset.sum_congr add_zero Finset.sum_centroidWeights_eq_one_of_nonempty RCLike.charZero_rclike Finset.sum_indicator_subset Finset.subset_univ
sum_circumcenterWeightsWithCircumcenter 📖	mathematical	—	Finset.sum PointsWithCircumcenterIndex Real Real.instAddCommMonoid Finset.univ instFintypePointsWithCircumcenterIndex circumcenterWeightsWithCircumcenter Real.instOne	—	Finset.sum_congr Finset.sum_ite_eq'
sum_pointWeightsWithCircumcenter 📖	mathematical	—	Finset.sum PointsWithCircumcenterIndex Real Real.instAddCommMonoid Finset.univ instFintypePointsWithCircumcenterIndex pointWeightsWithCircumcenter Real.instOne	—	Finset.sum_congr Finset.sum_ite_eq'
sum_pointsWithCircumcenter 📖	mathematical	—	Finset.sum PointsWithCircumcenterIndex Finset.univ instFintypePointsWithCircumcenterIndex AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Fin.fintype PointsWithCircumcenterIndex.pointIndex PointsWithCircumcenterIndex.circumcenterIndex	—	Finset.ext Finset.mem_insert_of_mem Finset.mem_map_of_mem Finset.mem_univ Finset.mem_insert_self add_comm Finset.sum_map Finset.sum_insert
sum_reflectionCircumcenterWeightsWithCircumcenter 📖	mathematical	—	Finset.sum PointsWithCircumcenterIndex Real Real.instAddCommMonoid Finset.univ instFintypePointsWithCircumcenterIndex reflectionCircumcenterWeightsWithCircumcenter Real.instOne	—	sum_pointsWithCircumcenter Finset.sum_congr Finset.sum_ite Finset.sum_const Finset.filter_or Finset.filter_eq' Finset.card_union_of_disjoint Mathlib.Meta.NormNum.instAtLeastTwo Finset.card_singleton Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat nsmul_eq_mul Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_natCast Nat.cast_one Finset.filter.congr_simp nsmul_zero add_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_neg

AffineIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsUnique_dist_eq 📖	mathematical	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	ExistsUnique EuclideanGeometry.Sphere AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range EuclideanGeometry.Sphere.center Set Set.instHasSubset Metric.sphere EuclideanGeometry.Sphere.radius	—	nonempty_fintype Fintype.card_pos_iff Fintype.card_eq_one_iff Set.range_unique Metric.sphere_zero dist_self Fintype.card_of_subtype Finset.filter_not Finset.filter_eq' Finset.mem_univ Finset.card_sdiff Finset.card_univ Finset.inter_univ Finset.card_singleton add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid subtype Subtype.finite Set.image_eq_range Set.image_univ Set.image_insert_eq Set.ext affineSpan_insert_affineSpan EuclideanGeometry.existsUnique_dist_eq_of_insert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Set.range_nonempty subset_affineSpan notMem_affineSpan_diff Real.instNontrivial

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circumcenter_eq_of_cospherical 📖	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 Cospherical Set Set.instHasSubset Set.range Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Affine.Simplex.circumcenter	—	exists_circumcenter_eq_of_cospherical
circumcenter_eq_of_cospherical_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction Real.semiring Submodule.addCommMonoid Submodule.module Cospherical Set.range Affine.Simplex.points	Affine.Simplex.circumcenter	—	exists_circumcenter_eq_of_cospherical_subset
circumradius_eq_of_cospherical 📖	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 Cospherical Set Set.instHasSubset Set.range Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Affine.Simplex.circumradius	—	exists_circumradius_eq_of_cospherical
circumradius_eq_of_cospherical_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction Real.semiring Submodule.addCommMonoid Submodule.module Cospherical Set.range Affine.Simplex.points	Affine.Simplex.circumradius	—	exists_circumradius_eq_of_cospherical_subset
circumsphere_eq_of_cospherical 📖	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 Cospherical Set Set.instHasSubset Set.range Affine.Simplex.points Real.instRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Affine.Simplex.circumsphere	—	exists_circumsphere_eq_of_cospherical
circumsphere_eq_of_cospherical_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction Real.semiring Submodule.addCommMonoid Submodule.module Cospherical Set.range Affine.Simplex.points	Affine.Simplex.circumsphere	—	exists_circumsphere_eq_of_cospherical_subset
cospherical_iff_exists_mem_of_complete 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike	Cospherical SetLike.instMembership Dist.dist PseudoMetricSpace.toDist	—	orthogonalProjection_mem exists_dist_eq_iff_exists_dist_orthogonalProjection_eq
cospherical_iff_exists_mem_of_finiteDimensional 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike	Cospherical SetLike.instMembership Dist.dist PseudoMetricSpace.toDist	—	cospherical_iff_exists_mem_of_complete Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule
eq_or_eq_reflection_of_dist_eq 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.range Affine.Simplex.points Dist.dist PseudoMetricSpace.toDist	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Submodule.HasOrthogonalProjection.ofCompleteSpace AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing complete_of_proper Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Real.instDivisionRing Finite.of_fintype Fin.fintype	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Finite.of_fintype AffineSubspace.mem_affineSpan_insert_iff orthogonalProjection_mem affineSpan_insert_affineSpan mem_affineSpan Set.mem_range_self Affine.Simplex.dist_circumcenter_sq_eq_sq_sub_circumradius Affine.Simplex.orthogonalProjectionSpan.eq_1 vsub_self smul_zero mul_self_eq_mul_self_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain mul_assoc real_inner_smul_right real_inner_smul_left real_inner_self_eq_norm_mul_norm vadd_vsub dist_eq_norm_vsub reflection_vadd_smul_vsub_orthogonalProjection Affine.Simplex.circumcenter_mem_affineSpan neg_smul Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection
existsUnique_dist_eq_of_insert 📖	mathematical	Set.Nonempty Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike SetLike.instMembership ExistsUnique Sphere Sphere.center Metric.sphere Sphere.radius	affineSpan Set.instInsert	—	Set.Nonempty.to_subtype Set.Nonempty.mono dist_orthogonalProjection_ne_zero_of_notMem Nat.instAtLeastTwoHAddOfNat one_smul vsub_vadd AffineSubspace.vadd_mem_of_mem_direction direction_affineSpan Submodule.smul_mem vsub_mem_vectorSpan Set.mem_insert Set.mem_insert_of_mem orthogonalProjection_mem mem_affineSpan Sphere.mem_coe mem_sphere mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing dist_nonneg Real.sqrt_nonneg Real.mul_self_sqrt add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_self_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd vsub_orthogonalProjection_mem_direction_orthogonal Real.norm_eq_abs abs_mul_abs_self dist_eq_norm_vsub dist_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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'_ofNat Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr 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.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq orthogonalProjection_vadd_smul_vsub_orthogonalProjection dist_of_mem_subset_mk_sphere vadd_vsub norm_smul NormedSpace.toNormSMulClass abs_div abs_of_nonneg div_mul_cancel₀ AffineSubspace.mem_affineSpan_insert_iff exists_dist_eq_iff_exists_dist_orthogonalProjection_eq mul_assoc mul_comm
exists_circumcenter_eq_of_cospherical 📖	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 Cospherical	Affine.Simplex.circumcenter	—	exists_circumcenter_eq_of_cospherical_subset Set.subset_univ AffineSubspace.instNonemptySubtypeMemTop FiniteDimensional.finiteDimensional_submodule AffineSubspace.direction_top finrank_top
exists_circumcenter_eq_of_cospherical_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction Real.semiring Submodule.addCommMonoid Submodule.module Cospherical	Affine.Simplex.circumcenter	—	cospherical_iff_exists_mem_of_finiteDimensional AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one Affine.Simplex.independent affineSpan_le_of_subset_coe HasSubset.Subset.trans Set.instIsTransSubset Fintype.card_fin Affine.Simplex.eq_circumcenter_of_dist_eq Set.mem_range_self
exists_circumradius_eq_of_cospherical 📖	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 Cospherical	Affine.Simplex.circumradius	—	exists_circumradius_eq_of_cospherical_subset Set.subset_univ AffineSubspace.instNonemptySubtypeMemTop FiniteDimensional.finiteDimensional_submodule AffineSubspace.direction_top finrank_top
exists_circumradius_eq_of_cospherical_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction Real.semiring Submodule.addCommMonoid Submodule.module Cospherical	Affine.Simplex.circumradius	—	cospherical_iff_exists_mem_of_finiteDimensional AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one Affine.Simplex.independent affineSpan_le_of_subset_coe HasSubset.Subset.trans Set.instIsTransSubset Fintype.card_fin Affine.Simplex.eq_circumradius_of_dist_eq Set.mem_range_self
exists_circumsphere_eq_of_cospherical 📖	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 Cospherical	Affine.Simplex.circumsphere	—	exists_circumsphere_eq_of_cospherical_subset Set.subset_univ AffineSubspace.instNonemptySubtypeMemTop FiniteDimensional.finiteDimensional_submodule AffineSubspace.direction_top finrank_top
exists_circumsphere_eq_of_cospherical_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction Real.semiring Submodule.addCommMonoid Submodule.module Cospherical	Affine.Simplex.circumsphere	—	exists_circumradius_eq_of_cospherical_subset exists_circumcenter_eq_of_cospherical_subset Sphere.ext

---

← Back to Index