Incenter

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

Statistics

Metric	Count
Definitions ExcenterExists, excenter, excenterWeights, excenterWeightsUnnorm, exradius, exsphere, incenter, inradius, insphere, touchpoint, touchpointWeights	11
Theorems affineCombination_eq_excenter_iff, affineSpan_faceOpposite_eq_orthRadius, dist_excenter, dist_excenter_eq_dist_excenter, excenterWeights_eq_excenterWeights_iff, excenterWeights_ne_zero, excenter_eq_excenter_iff, excenter_eq_incenter_iff, excenter_map, excenter_mem_affineSpan_range, excenter_ne_point, excenter_notMem_affineSpan_face, excenter_notMem_affineSpan_faceOpposite, excenter_notMem_affineSpan_pair, excenter_restrict, exradius_pos, isTangentAt_exsphere_iff_eq_touchpoint, isTangentAt_touchpoint, sOppSide_excenter_point_iff, sOppSide_point_excenter_iff, sSameSide_excenter_point_iff, sSameSide_point_excenter_iff, sign_signedInfDist_excenter, sign_signedInfDist_lineMap_excenter_touchpoint, sign_signedInfDist_touchpoint, sign_touchpointWeights, signedInfDist_excenter, signedInfDist_excenter_eq_mul_sum_inv, sum_excenterWeights_eq_one, touchpointWeights_map, touchpointWeights_restrict, touchpoint_injective, touchpoint_map, touchpoint_mem_exsphere, touchpoint_ne_point, touchpoint_notMem_affineSpan_of_ne, touchpoint_restrict, affineCombination_eq_touchpoint_iff, affineCombination_touchpointWeights, affineSpan_faceOpposite_eq_orthRadius_insphere, dist_incenter, dist_incenter_eq_dist_incenter, eq_touchpoint_of_isTangentAt_exsphere, excenterExists_compl, excenterExists_empty, excenterExists_map, excenterExists_reindex, excenterExists_restrict, excenterExists_singleton, excenterWeightsUnnorm_compl, excenterWeightsUnnorm_empty_apply, excenterWeightsUnnorm_map, excenterWeightsUnnorm_ne_zero, excenterWeightsUnnorm_reindex, excenterWeightsUnnorm_restrict, excenterWeights_compl, excenterWeights_empty_lt_inv_two, excenterWeights_empty_pos, excenterWeights_map, excenterWeights_reindex, excenterWeights_restrict, excenter_compl, excenter_empty, excenter_eq_affineCombination, excenter_reindex, excenter_singleton_injective, excenter_singleton_mem_affineSpan_range, excenter_singleton_ne_incenter, excenter_univ, exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, exists_forall_signedInfDist_eq_iff_eq_incenter, exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, exradius_compl, exradius_empty, exradius_eq_abs_inv_sum, exradius_map, exradius_nonneg, exradius_reindex, exradius_restrict, exradius_singleton_pos, exradius_univ, exsphere_center, exsphere_compl, exsphere_empty, exsphere_radius, exsphere_reindex, exsphere_univ, incenter_eq_affineCombination, incenter_map, incenter_mem_affineSpan_range, incenter_mem_interior, incenter_ne_point, incenter_notMem_affineSpan_face, incenter_notMem_affineSpan_faceOpposite, incenter_notMem_affineSpan_pair, incenter_reindex, incenter_restrict, inradius_eq_abs_inv_sum, inradius_map, inradius_pos, inradius_reindex, inradius_restrict, insphere_center, insphere_radius, insphere_reindex, inv_height_eq_sum_mul_inv_dist, inv_height_lt_sum_inv_height, isTangentAt_insphere_iff_eq_touchpoint, isTangentAt_insphere_touchpoint, sOppSide_excenter_singleton_point, sOppSide_point_excenter_singleton, sSameSide_excenter_singleton_point, sSameSide_incenter_point, sSameSide_point_excenter_singleton, sSameSide_point_incenter, sign_excenterWeights_empty, sign_excenterWeights_singleton_neg, sign_excenterWeights_singleton_pos, sign_signedInfDist_incenter, sign_signedInfDist_lineMap_incenter_touchpoint, sign_signedInfDist_touchpoint_empty, sign_touchpointWeights_empty, sign_touchpointWeights_singleton_neg, sign_touchpointWeights_singleton_pos, signedInfDist_incenter, sum_excenterWeights, sum_excenterWeightsUnnorm_empty_pos, sum_excenterWeightsUnnorm_singleton_pos, sum_excenterWeights_eq_one_iff, sum_inv_height_sq_smul_vsub_eq_zero, sum_touchpointWeights, touchpointWeights_empty_pos, touchpointWeights_eq_zero, touchpointWeights_reindex, touchpointWeights_singleton_neg, touchpointWeights_singleton_pos, touchpoint_empty_injective, touchpoint_empty_mem_interior_faceOpposite, touchpoint_empty_ne_point, touchpoint_empty_notMem_affineSpan_of_ne, touchpoint_eq_point_rev, touchpoint_mem_affineSpan, touchpoint_mem_affineSpan_simplex, touchpoint_mem_insphere, touchpoint_reindex, touchpoint_singleton_mem_interior_faceOpposite, affineSpan_pair_eq_orthRadius, affineSpan_pair_eq_orthRadius_insphere, excenterExists, excenter_eq_incenter_or_excenter_singleton, excenter_eq_incenter_or_excenter_singleton_of_ne, sOppSide_affineSpan_pair_excenter_singleton_point, sOppSide_affineSpan_pair_point_excenter_singleton, sSameSide_affineSpan_pair_excenter_singleton_point, sSameSide_affineSpan_pair_incenter_point, sSameSide_affineSpan_pair_point_excenter_singleton, sSameSide_affineSpan_pair_point_incenter, sbtw_touchpoint_empty, sbtw_touchpoint_singleton, touchpoint_singleton_sbtw	160
Total	171

Affine.Simplex

Definitions

Name	Category	Theorems
ExcenterExists 📖	MathDef	11 math math: excenterExists_reindex, excenterExists_map, exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, sum_excenterWeights_eq_one_iff, excenterExists_compl, sum_excenterWeights, exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, excenterExists_empty, excenterExists_singleton, Affine.Triangle.excenterExists, excenterExists_restrict
excenter 📖	CompOp	40 math math: ExcenterExists.excenter_notMem_affineSpan_face, sSameSide_excenter_singleton_point, ExcenterExists.excenter_notMem_affineSpan_faceOpposite, excenter_singleton_mem_affineSpan_range, ExcenterExists.affineCombination_eq_excenter_iff, excenter_singleton_injective, ExcenterExists.excenter_map, excenter_eq_affineCombination, ExcenterExists.dist_excenter, Affine.Triangle.excenter_eq_incenter_or_excenter_singleton_of_ne, ExcenterExists.excenter_eq_incenter_iff, ExcenterExists.sign_signedInfDist_touchpoint, ExcenterExists.dist_excenter_eq_dist_excenter, excenter_empty, ExcenterExists.sOppSide_excenter_point_iff, Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point, ExcenterExists.excenter_restrict, ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, Affine.Triangle.excenter_eq_incenter_or_excenter_singleton, exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, sOppSide_excenter_singleton_point, ExcenterExists.sOppSide_point_excenter_iff, ExcenterExists.excenter_notMem_affineSpan_pair, sOppSide_point_excenter_singleton, ExcenterExists.excenter_mem_affineSpan_range, Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton, ExcenterExists.signedInfDist_excenter, exsphere_center, sSameSide_point_excenter_singleton, Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton, ExcenterExists.sign_signedInfDist_excenter, ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point, excenter_univ, excenter_reindex, excenter_compl, ExcenterExists.excenter_eq_excenter_iff, ExcenterExists.sSameSide_excenter_point_iff, ExcenterExists.sSameSide_point_excenter_iff
excenterWeights 📖	CompOp	22 math math: sign_excenterWeights_singleton_pos, ExcenterExists.affineCombination_eq_excenter_iff, excenter_eq_affineCombination, excenterWeights_reindex, ExcenterExists.sOppSide_excenter_point_iff, ExcenterExists.excenterWeights_eq_excenterWeights_iff, sign_excenterWeights_singleton_neg, excenterWeights_empty_lt_inv_two, ExcenterExists.sOppSide_point_excenter_iff, sum_excenterWeights_eq_one_iff, ExcenterExists.sign_touchpointWeights, incenter_eq_affineCombination, excenterWeights_restrict, sign_excenterWeights_empty, ExcenterExists.sum_excenterWeights_eq_one, excenterWeights_map, excenterWeights_empty_pos, ExcenterExists.sign_signedInfDist_excenter, sum_excenterWeights, excenterWeights_compl, ExcenterExists.sSameSide_excenter_point_iff, ExcenterExists.sSameSide_point_excenter_iff
excenterWeightsUnnorm 📖	CompOp	11 math math: excenterWeightsUnnorm_reindex, excenterWeightsUnnorm_map, sum_excenterWeightsUnnorm_singleton_pos, excenterWeightsUnnorm_empty_apply, inradius_eq_abs_inv_sum, exradius_eq_abs_inv_sum, excenterWeightsUnnorm_restrict, ExcenterExists.signedInfDist_excenter, sum_excenterWeightsUnnorm_empty_pos, ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, excenterWeightsUnnorm_compl
exradius 📖	CompOp	13 math math: ExcenterExists.dist_excenter, exradius_map, exradius_nonneg, exradius_empty, exradius_reindex, exradius_restrict, exradius_singleton_pos, exradius_compl, exradius_eq_abs_inv_sum, ExcenterExists.signedInfDist_excenter, exradius_univ, exsphere_radius, ExcenterExists.exradius_pos
exsphere 📖	CompOp	11 math math: ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, ExcenterExists.isTangentAt_touchpoint, Affine.Triangle.affineSpan_pair_eq_orthRadius, exsphere_reindex, exsphere_compl, ExcenterExists.touchpoint_mem_exsphere, ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, exsphere_univ, exsphere_empty, exsphere_center, exsphere_radius
incenter 📖	CompOp	26 math math: incenter_map, Affine.Triangle.sSameSide_affineSpan_pair_point_incenter, sign_signedInfDist_lineMap_incenter_touchpoint, sSameSide_incenter_point, Affine.Triangle.excenter_eq_incenter_or_excenter_singleton_of_ne, ExcenterExists.excenter_eq_incenter_iff, excenter_empty, incenter_mem_interior, incenter_notMem_affineSpan_face, dist_incenter_eq_dist_incenter, Affine.Triangle.excenter_eq_incenter_or_excenter_singleton, incenter_restrict, incenter_eq_affineCombination, exists_forall_signedInfDist_eq_iff_eq_incenter, sign_signedInfDist_touchpoint_empty, incenter_mem_affineSpan_range, incenter_notMem_affineSpan_pair, incenter_reindex, sign_signedInfDist_incenter, insphere_center, dist_incenter, excenter_univ, Affine.Triangle.sSameSide_affineSpan_pair_incenter_point, incenter_notMem_affineSpan_faceOpposite, sSameSide_point_incenter, signedInfDist_incenter
inradius 📖	CompOp	10 math math: insphere_radius, inradius_reindex, exradius_empty, inradius_eq_abs_inv_sum, inradius_restrict, exradius_univ, inradius_pos, dist_incenter, inradius_map, signedInfDist_incenter
insphere 📖	CompOp	10 math math: isTangentAt_insphere_iff_eq_touchpoint, insphere_radius, isTangentAt_insphere_touchpoint, affineSpan_faceOpposite_eq_orthRadius_insphere, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, exsphere_univ, exsphere_empty, insphere_center, touchpoint_mem_insphere, insphere_reindex
touchpoint 📖	CompOp	36 math math: isTangentAt_insphere_iff_eq_touchpoint, Affine.Triangle.sbtw_touchpoint_singleton, touchpoint_empty_injective, sign_signedInfDist_lineMap_incenter_touchpoint, ExcenterExists.touchpoint_map, ExcenterExists.touchpoint_notMem_affineSpan_of_ne, touchpoint_singleton_mem_interior_faceOpposite, isTangentAt_insphere_touchpoint, ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, ExcenterExists.dist_excenter, affineSpan_faceOpposite_eq_orthRadius_insphere, Affine.Triangle.touchpoint_singleton_sbtw, ExcenterExists.sign_signedInfDist_touchpoint, ExcenterExists.dist_excenter_eq_dist_excenter, ExcenterExists.isTangentAt_touchpoint, Affine.Triangle.affineSpan_pair_eq_orthRadius, ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, dist_incenter_eq_dist_incenter, ExcenterExists.touchpoint_mem_exsphere, touchpoint_mem_affineSpan, affineCombination_eq_touchpoint_iff, ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, touchpoint_reindex, sign_signedInfDist_touchpoint_empty, touchpoint_eq_point_rev, ExcenterExists.touchpoint_restrict, affineCombination_touchpointWeights, Affine.Triangle.sbtw_touchpoint_empty, touchpoint_empty_notMem_affineSpan_of_ne, ExcenterExists.touchpoint_injective, touchpoint_mem_affineSpan_simplex, dist_incenter, touchpoint_empty_mem_interior_faceOpposite, touchpoint_mem_insphere, eq_touchpoint_of_isTangentAt_exsphere
touchpointWeights 📖	CompOp	14 math math: sign_touchpointWeights_empty, touchpointWeights_empty_pos, ExcenterExists.touchpointWeights_restrict, touchpointWeights_reindex, affineCombination_eq_touchpoint_iff, ExcenterExists.sign_touchpointWeights, sign_touchpointWeights_singleton_pos, sign_touchpointWeights_singleton_neg, ExcenterExists.touchpointWeights_map, affineCombination_touchpointWeights, touchpointWeights_singleton_neg, touchpointWeights_eq_zero, sum_touchpointWeights, touchpointWeights_singleton_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineCombination_eq_touchpoint_iff 📖	mathematical	Finset.sum Real Real.instAddCommMonoid Finset.univ Fin.fintype Real.instOne	DFunLike.coe AffineMap Real.instRing Pi.addCommGroup 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 points touchpoint touchpointWeights	—	affineCombination_touchpointWeights affineIndependent_iff_eq_of_fintype_affineCombination_eq independent sum_touchpointWeights
affineCombination_touchpointWeights 📖	mathematical	—	DFunLike.coe AffineMap Real Real.instRing Pi.addCommGroup 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 Fin.fintype points touchpointWeights touchpoint	—	eq_affineCombination_of_mem_affineSpan_of_fintype touchpoint_mem_affineSpan_simplex
affineSpan_faceOpposite_eq_orthRadius_insphere 📖	mathematical	—	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range points faceOpposite EuclideanGeometry.Sphere.orthRadius insphere touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.affineSpan_faceOpposite_eq_orthRadius excenterExists_empty
dist_incenter 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace incenter touchpoint Finset Finset.instEmptyCollection inradius	—	ExcenterExists.dist_excenter excenterExists_empty
dist_incenter_eq_dist_incenter 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace incenter touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.dist_excenter_eq_dist_excenter excenterExists_empty
eq_touchpoint_of_isTangentAt_exsphere 📖	mathematical	EuclideanGeometry.Sphere.IsTangentAt exsphere affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range points faceOpposite	touchpoint	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Finite.of_fintype EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection touchpoint.eq_1 orthogonalProjectionSpan.eq_1 excenter.eq_1
excenterExists_compl 📖	mathematical	—	ExcenterExists Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	Finset.sum_congr excenterWeightsUnnorm_compl Finset.sum_neg_distrib
excenterExists_empty 📖	mathematical	—	ExcenterExists Finset Finset.instEmptyCollection	—	LT.lt.ne' sum_excenterWeightsUnnorm_empty_pos
excenterExists_map 📖	mathematical	—	ExcenterExists 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 Finset.sum_congr excenterWeightsUnnorm_map
excenterExists_reindex 📖	mathematical	—	ExcenterExists reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm	—	Finset.sum_congr excenterWeightsUnnorm_reindex Finset.sum_comp_equiv Finset.map_univ_equiv
excenterExists_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	ExcenterExists 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 Finset.sum_congr excenterWeightsUnnorm_restrict
excenterExists_singleton 📖	mathematical	—	ExcenterExists Finset Finset.instSingleton	—	LT.lt.ne' sum_excenterWeightsUnnorm_singleton_pos
excenterWeightsUnnorm_compl 📖	mathematical	—	excenterWeightsUnnorm Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Pi.instNeg Real Real.instNeg	—	one_mul neg_mul neg_neg
excenterWeightsUnnorm_empty_apply 📖	mathematical	—	excenterWeightsUnnorm Finset Finset.instEmptyCollection Real Real.instInv height	—	one_mul
excenterWeightsUnnorm_map 📖	mathematical	—	excenterWeightsUnnorm 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 height_map ite_mul neg_mul one_mul
excenterWeightsUnnorm_ne_zero 📖	—	—	—	—	excenterWeightsUnnorm.eq_1 mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne' height_pos
excenterWeightsUnnorm_reindex 📖	mathematical	—	excenterWeightsUnnorm reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	height_reindex ite_mul neg_mul one_mul Equiv.apply_symm_apply
excenterWeightsUnnorm_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	excenterWeightsUnnorm 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 height_restrict ite_mul neg_mul one_mul
excenterWeights_compl 📖	mathematical	—	excenterWeights Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	Finset.sum_congr excenterWeightsUnnorm_compl Finset.sum_neg_distrib inv_neg smul_neg neg_smul neg_neg
excenterWeights_empty_lt_inv_two 📖	mathematical	—	Real Real.instLT excenterWeights Finset Finset.instEmptyCollection Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	inv_height_lt_sum_inv_height add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Finset.compl_singleton Finset.filter_ne' Nat.instAtLeastTwoHAddOfNat two_mul Finset.sum_singleton div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Finset.sum_pos Real.instIsOrderedCancelAddMonoid inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono height_pos Finset.univ_nonempty lt_inv_mul_iff₀ zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Finset.sum_add_sum_compl Finset.sum_congr one_mul div_eq_inv_mul
excenterWeights_empty_pos 📖	mathematical	—	Real Real.instLT Real.instZero excenterWeights Finset Finset.instEmptyCollection	—	Finset.sum_congr excenterWeightsUnnorm_empty_apply mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Finset.sum_pos Real.instIsOrderedCancelAddMonoid height_pos Finset.univ_nonempty
excenterWeights_map 📖	mathematical	—	excenterWeights 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 Finset.sum_congr excenterWeightsUnnorm_map
excenterWeights_reindex 📖	mathematical	—	excenterWeights reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Finset.sum_congr excenterWeightsUnnorm_reindex Finset.sum_comp_equiv Finset.map_univ_equiv
excenterWeights_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	excenterWeights 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 Finset.sum_congr excenterWeightsUnnorm_restrict
excenter_compl 📖	mathematical	—	excenter Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	exsphere_compl
excenter_empty 📖	mathematical	—	excenter Finset Finset.instEmptyCollection incenter	—	—
excenter_eq_affineCombination 📖	mathematical	—	excenter DFunLike.coe AffineMap Real Real.instRing Pi.addCommGroup 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 Fin.fintype points excenterWeights	—	—
excenter_reindex 📖	mathematical	—	excenter reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm	—	exsphere_reindex
excenter_singleton_injective 📖	mathematical	—	excenter Finset Finset.instSingleton	—	ExcenterExists.excenter_eq_excenter_iff excenterExists_singleton Nat.AtLeastTwo.prop Fin.exists_ne_and_ne_of_two_lt Finset.ext_iff
excenter_singleton_mem_affineSpan_range 📖	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 excenter Finset Finset.instSingleton	—	ExcenterExists.excenter_mem_affineSpan_range excenterExists_singleton
excenter_singleton_ne_incenter 📖	—	—	—	—	Fin.instNontrivial Nat.instAtLeastTwoHAddOfNat ExcenterExists.excenter_eq_incenter_iff excenterExists_singleton
excenter_univ 📖	mathematical	—	excenter Finset.univ Fin.fintype incenter	—	excenter.eq_1 exsphere_univ insphere_center
exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter 📖	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 NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField faceOpposite 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 ExcenterExists excenter	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange abs_signedInfDist_eq_dist_of_mem_affineSpan_range eq_or_eq_neg_of_abs_eq exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter ite_mul neg_mul one_mul abs_ite abs_neg
exists_forall_signedInfDist_eq_iff_eq_incenter 📖	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	DFunLike.coe ContinuousAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike signedInfDist incenter	—	one_mul exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter
exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter 📖	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	DFunLike.coe ContinuousAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike signedInfDist Real.instMul Finset Finset.instMembership Finset.decidableMem Real.instNeg Real.instOne ExcenterExists excenter	—	eq_affineCombination_of_mem_affineSpan_of_fintype altitudeFoot.eq_1 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange signedInfDist_affineCombination eq_div_iff LT.lt.ne' height_pos height.eq_1 mul_comm div_eq_mul_inv mul_assoc orthogonalProjectionSpan.eq_1 eq_inv_of_mul_eq_one_left Finset.sum_congr sum_excenterWeights_eq_one_iff ExcenterExists.signedInfDist_excenter ite_mul neg_mul one_mul
exradius_compl 📖	mathematical	—	exradius Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	exsphere_compl
exradius_empty 📖	mathematical	—	exradius Finset Finset.instEmptyCollection inradius	—	—
exradius_eq_abs_inv_sum 📖	mathematical	—	exradius abs Real Real.lattice Real.instAddGroup Real.instInv Finset.sum Real.instAddCommMonoid Finset.univ Fin.fintype excenterWeightsUnnorm	—	—
exradius_map 📖	mathematical	—	exradius 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 AffineIsometry.coe_toAffineMap excenterWeights_map Finset.sum_congr excenterWeightsUnnorm_map abs_inv Real.instIsStrictOrderedRing
exradius_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero exradius	—	abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
exradius_reindex 📖	mathematical	—	exradius reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm	—	exsphere_reindex
exradius_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	exradius 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 excenterWeights_restrict Finset.sum_congr excenterWeightsUnnorm_restrict abs_inv Real.instIsStrictOrderedRing
exradius_singleton_pos 📖	mathematical	—	Real Real.instLT Real.instZero exradius Finset Finset.instSingleton	—	ExcenterExists.exradius_pos excenterExists_singleton
exradius_univ 📖	mathematical	—	exradius Finset.univ Fin.fintype inradius	—	exradius.eq_1 exsphere_univ insphere_radius
exsphere_center 📖	mathematical	—	EuclideanGeometry.Sphere.center exsphere excenter	—	—
exsphere_compl 📖	mathematical	—	exsphere Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	excenterWeights_compl Finset.sum_congr excenterWeightsUnnorm_compl Finset.sum_neg_distrib inv_neg abs_neg abs_inv Real.instIsStrictOrderedRing
exsphere_empty 📖	mathematical	—	exsphere Finset Finset.instEmptyCollection insphere	—	—
exsphere_radius 📖	mathematical	—	EuclideanGeometry.Sphere.radius exsphere exradius	—	—
exsphere_reindex 📖	mathematical	—	exsphere reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm	—	Finset.sum_congr excenterWeightsUnnorm_reindex excenterWeights_reindex Finset.sum_comp_equiv Finset.map_univ_equiv abs_inv Real.instIsStrictOrderedRing
exsphere_univ 📖	mathematical	—	exsphere Finset.univ Fin.fintype insphere	—	Finset.compl_empty exsphere_compl insphere.eq_1
incenter_eq_affineCombination 📖	mathematical	—	incenter DFunLike.coe AffineMap Real Real.instRing Pi.addCommGroup 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 Fin.fintype points excenterWeights Finset Finset.instEmptyCollection	—	—
incenter_map 📖	mathematical	—	incenter 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	—	ExcenterExists.excenter_map excenterExists_empty
incenter_mem_affineSpan_range 📖	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 incenter	—	ExcenterExists.excenter_mem_affineSpan_range excenterExists_empty
incenter_mem_interior 📖	mathematical	—	Set Set.instMembership interior Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.partialOrder incenter	—	ExcenterExists.sum_excenterWeights_eq_one excenterExists_empty incenter_eq_affineCombination affineCombination_mem_interior_iff excenterWeights_empty_pos exists_ne Fin.instNontrivial Nat.instAtLeastTwoHAddOfNat ne_of_gt add_comm lt_imp_lt_of_le_of_le le_refl add_assoc lt_add_iff_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le add_pos_of_pos_of_nonneg Finset.sum_nonneg LT.lt.le Finset.sum_pair Finset.sum_add_sum_compl
incenter_ne_point 📖	—	—	—	—	ExcenterExists.excenter_ne_point excenterExists_empty
incenter_notMem_affineSpan_face 📖	mathematical	Finset.card	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 face incenter	—	ExcenterExists.excenter_notMem_affineSpan_face excenterExists_empty
incenter_notMem_affineSpan_faceOpposite 📖	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 faceOpposite incenter	—	ExcenterExists.excenter_notMem_affineSpan_faceOpposite excenterExists_empty
incenter_notMem_affineSpan_pair 📖	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 points Set.instSingletonSet incenter	—	ExcenterExists.excenter_notMem_affineSpan_pair excenterExists_empty
incenter_reindex 📖	mathematical	—	incenter reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	exsphere_reindex
incenter_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 incenter 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	—	ExcenterExists.excenter_restrict excenterExists_empty
inradius_eq_abs_inv_sum 📖	mathematical	—	inradius abs Real Real.lattice Real.instAddGroup Real.instInv Finset.sum Real.instAddCommMonoid Finset.univ Fin.fintype excenterWeightsUnnorm Finset Finset.instEmptyCollection	—	—
inradius_map 📖	mathematical	—	inradius 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 exradius_map
inradius_pos 📖	mathematical	—	Real Real.instLT Real.instZero inradius	—	ExcenterExists.exradius_pos excenterExists_empty
inradius_reindex 📖	mathematical	—	inradius reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	exsphere_reindex
inradius_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	inradius 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 exradius_restrict
insphere_center 📖	mathematical	—	EuclideanGeometry.Sphere.center insphere incenter	—	—
insphere_radius 📖	mathematical	—	EuclideanGeometry.Sphere.radius insphere inradius	—	—
insphere_reindex 📖	mathematical	—	insphere reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	exsphere_reindex
inv_height_eq_sum_mul_inv_dist 📖	mathematical	—	Real Real.instInv height Finset.sum Real.instAddCommMonoid Finset.filter Finset.univ Fin.fintype Real.instMul Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot	—	sub_eq_zero Finset.sum_congr neg_mul Finset.sum_neg_distrib sub_neg_eq_add Finset.filter_ne' Finset.sum_erase_eq_sub Finset.mem_univ real_inner_self_eq_norm_mul_norm dist_eq_norm_vsub div_self NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass one_mul add_sub_cancel sum_inv_height_sq_smul_vsub_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.pow_congr 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_pow Mathlib.Tactic.Ring.pow_zero inner_smul_right inner_zero_right MulZeroClass.mul_zero Finset.mul_sum inner_sum
inv_height_lt_sum_inv_height 📖	mathematical	—	Real Real.instLT Real.instInv height Finset.sum Real.instAddCommMonoid Finset.filter Finset.univ Fin.fintype	—	inv_height_eq_sum_mul_inv_dist Finset.sum_lt_sum_of_nonempty Real.instIsOrderedCancelAddMonoid Finset.filter_ne' Finset.card_ne_zero Finset.card_erase_of_mem Fintype.card_fin add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_lt_of_lt_one_left IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add neg_one_lt_inner_vsub_altitudeFoot_div
isTangentAt_insphere_iff_eq_touchpoint 📖	mathematical	—	EuclideanGeometry.Sphere.IsTangentAt insphere affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range points faceOpposite touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint excenterExists_empty
isTangentAt_insphere_touchpoint 📖	mathematical	—	EuclideanGeometry.Sphere.IsTangentAt insphere touchpoint Finset Finset.instEmptyCollection affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range points faceOpposite	—	ExcenterExists.isTangentAt_touchpoint excenterExists_empty
sOppSide_excenter_singleton_point 📖	mathematical	—	AffineSubspace.SOppSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range points faceOpposite excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing ExcenterExists.sOppSide_excenter_point_iff excenterExists_singleton sign_eq_neg_one_iff sign_excenterWeights_singleton_neg
sOppSide_point_excenter_singleton 📖	mathematical	—	AffineSubspace.SOppSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range points faceOpposite excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing ExcenterExists.sOppSide_point_excenter_iff excenterExists_singleton sign_eq_neg_one_iff sign_excenterWeights_singleton_neg
sSameSide_excenter_singleton_point 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range points faceOpposite excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing ExcenterExists.sSameSide_excenter_point_iff excenterExists_singleton sign_eq_one_iff sign_excenterWeights_singleton_pos
sSameSide_incenter_point 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range points faceOpposite incenter	—	Real.instIsStrictOrderedRing ExcenterExists.sSameSide_excenter_point_iff excenterExists_empty excenterWeights_empty_pos
sSameSide_point_excenter_singleton 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range points faceOpposite excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing ExcenterExists.sSameSide_point_excenter_iff excenterExists_singleton sign_eq_one_iff sign_excenterWeights_singleton_pos
sSameSide_point_incenter 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range points faceOpposite incenter	—	Real.instIsStrictOrderedRing ExcenterExists.sSameSide_point_excenter_iff excenterExists_empty excenterWeights_empty_pos
sign_excenterWeights_empty 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT excenterWeights Finset Finset.instEmptyCollection SignType.instOne	—	sign_eq_one_iff excenterWeights_empty_pos
sign_excenterWeights_singleton_neg 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT excenterWeights Finset Finset.instSingleton SignType.instNeg SignType.instOne	—	sign_mul Real.instIsStrictOrderedRing sign_eq_one_iff inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sum_excenterWeightsUnnorm_singleton_pos neg_mul one_mul sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
sign_excenterWeights_singleton_pos 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT excenterWeights Finset Finset.instSingleton SignType.instOne	—	sign_mul Real.instIsStrictOrderedRing sign_eq_one_iff inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sum_excenterWeightsUnnorm_singleton_pos one_mul sign_pos
sign_signedInfDist_incenter 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT ContinuousAffineMap Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike signedInfDist incenter SignType.instOne	—	sign_excenterWeights_empty ExcenterExists.sign_signedInfDist_excenter excenterExists_empty
sign_signedInfDist_lineMap_incenter_touchpoint 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	DFunLike.coe OrderHom SignType PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT ContinuousAffineMap Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike signedInfDist AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap incenter touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint excenterExists_empty
sign_signedInfDist_touchpoint_empty 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT ContinuousAffineMap Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike signedInfDist touchpoint Finset Finset.instEmptyCollection incenter	—	ExcenterExists.sign_signedInfDist_touchpoint excenterExists_empty
sign_touchpointWeights_empty 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT touchpointWeights Finset Finset.instEmptyCollection SignType.instOne	—	ExcenterExists.sign_touchpointWeights excenterExists_empty sign_excenterWeights_empty
sign_touchpointWeights_singleton_neg 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT touchpointWeights Finset Finset.instSingleton SignType.instNeg SignType.instOne	—	ExcenterExists.sign_touchpointWeights excenterExists_singleton sign_excenterWeights_singleton_neg
sign_touchpointWeights_singleton_pos 📖	mathematical	—	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT touchpointWeights Finset Finset.instSingleton SignType.instOne	—	ExcenterExists.sign_touchpointWeights excenterExists_singleton sign_excenterWeights_singleton_pos
signedInfDist_incenter 📖	mathematical	—	DFunLike.coe ContinuousAffineMap Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike signedInfDist incenter inradius	—	incenter.eq_1 exsphere_center ExcenterExists.signedInfDist_excenter excenterExists_empty Finset.sum_congr excenterWeightsUnnorm_empty_apply sign_pos Finset.sum_pos Real.instIsOrderedCancelAddMonoid inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing height_pos Finset.univ_nonempty mul_one one_mul
sum_excenterWeights 📖	mathematical	—	Finset.sum Real Real.instAddCommMonoid Finset.univ Fin.fintype excenterWeights ExcenterExists Real.instOne Real.instZero	—	Finset.sum_congr inv_mul_cancel₀ inv_zero MulZeroClass.zero_mul Finset.sum_const_zero
sum_excenterWeightsUnnorm_empty_pos 📖	mathematical	—	Real Real.instLT Real.instZero Finset.sum Real.instAddCommMonoid Finset.univ Fin.fintype excenterWeightsUnnorm Finset Finset.instEmptyCollection	—	Finset.sum_congr excenterWeightsUnnorm_empty_apply Finset.sum_pos Real.instIsOrderedCancelAddMonoid inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing height_pos Finset.univ_nonempty
sum_excenterWeightsUnnorm_singleton_pos 📖	mathematical	—	Real Real.instLT Real.instZero Finset.sum Real.instAddCommMonoid Finset.univ Fin.fintype excenterWeightsUnnorm Finset Finset.instSingleton	—	Finset.sum_add_sum_compl Finset.sum_singleton excenterWeightsUnnorm.eq_1 neg_mul one_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_zero Finset.sum_congr Finset.ext Finset.mem_filter_univ inv_height_lt_sum_inv_height
sum_excenterWeights_eq_one_iff 📖	mathematical	—	Finset.sum Real Real.instAddCommMonoid Finset.univ Fin.fintype excenterWeights Real.instOne ExcenterExists	—	sum_excenterWeights NeZero.charZero_one RCLike.charZero_rclike
sum_inv_height_sq_smul_vsub_eq_zero 📖	mathematical	—	Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.univ Fin.fintype Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Monoid.toNatPow Real.instInv height VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup altitudeFoot NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Finset.add_sum_erase Finset.mem_univ Finset.mem_erase add_assoc Finset.sum_congr real_inner_smul_right Submodule.mem_orthogonal_singleton_iff_inner_right SetLike.le_def instIsConcreteLE Submodule.orthogonal_le Submodule.span_singleton_le_iff_mem direction_affineSpan vsub_mem_vectorSpan range_faceOpposite_points EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal MulZeroClass.mul_zero Finset.sum_const_zero inner_smul_right inner_vsub_vsub_altitudeFoot_eq_height_sq neg_vsub_eq_vsub_rev inner_neg_left mul_neg inv_pow inv_mul_cancel₀ isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat neg_add_cancel add_zero Submodule.mem_bot Submodule.inf_orthogonal_eq_bot Submodule.sum_smul_mem vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan mem_affineSpan Set.mem_range_self altitudeFoot_mem_affineSpan vectorSpan_range_eq_span_range_vsub_right_ne Submodule.span_range_eq_iSup Submodule.iInf_orthogonal Submodule.coe_iInf Set.mem_iInter inner_sum
sum_touchpointWeights 📖	mathematical	—	Finset.sum Real Real.instAddCommMonoid Finset.univ Fin.fintype touchpointWeights Real.instOne	—	eq_affineCombination_of_mem_affineSpan_of_fintype touchpoint_mem_affineSpan_simplex
touchpointWeights_empty_pos 📖	mathematical	—	Real Real.instLT Real.instZero touchpointWeights Finset Finset.instEmptyCollection	—	sign_touchpointWeights_empty
touchpointWeights_eq_zero 📖	mathematical	—	touchpointWeights Real Real.instZero	—	AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan independent sum_touchpointWeights affineCombination_touchpointWeights range_faceOpposite_points touchpoint_mem_affineSpan Finset.mem_univ Set.notMem_compl_iff Set.mem_singleton
touchpointWeights_reindex 📖	mathematical	—	touchpointWeights reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	affineCombination_eq_touchpoint_iff Finset.sum_comp_equiv Finset.sum_congr Finset.map_univ_equiv sum_touchpointWeights touchpoint_reindex affineCombination_touchpointWeights reindex.eq_1 Equiv.coe_toEmbedding Finset.affineCombination_map
touchpointWeights_singleton_neg 📖	mathematical	—	Real Real.instLT touchpointWeights Finset Finset.instSingleton Real.instZero	—	sign_touchpointWeights_singleton_neg
touchpointWeights_singleton_pos 📖	mathematical	—	Real Real.instLT Real.instZero touchpointWeights Finset Finset.instSingleton	—	sign_touchpointWeights_singleton_pos
touchpoint_empty_injective 📖	mathematical	—	touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.touchpoint_injective excenterExists_empty
touchpoint_empty_mem_interior_faceOpposite 📖	mathematical	—	Set Set.instMembership interior Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.partialOrder faceOpposite touchpoint Finset Finset.instEmptyCollection	—	faceOpposite.eq_1 affineCombination_touchpointWeights affineCombination_mem_interior_face_iff_pos Real.instIsOrderedAddMonoid Nat.AtLeastTwo.neZero_sub_one sum_touchpointWeights touchpointWeights_eq_zero touchpointWeights_empty_pos
touchpoint_empty_ne_point 📖	—	—	—	—	ExcenterExists.touchpoint_ne_point excenterExists_empty
touchpoint_empty_notMem_affineSpan_of_ne 📖	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 faceOpposite touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.touchpoint_notMem_affineSpan_of_ne excenterExists_empty
touchpoint_eq_point_rev 📖	mathematical	—	touchpoint points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	orthogonalProjectionSpan_faceOpposite_eq_point_rev
touchpoint_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 faceOpposite touchpoint	—	EuclideanGeometry.orthogonalProjection_mem
touchpoint_mem_affineSpan_simplex 📖	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 touchpoint	—	SetLike.le_def instIsConcreteLE affineSpan_mono range_faceOpposite_points Set.preimage_range touchpoint_mem_affineSpan
touchpoint_mem_insphere 📖	mathematical	—	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere insphere touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.touchpoint_mem_exsphere excenterExists_empty
touchpoint_reindex 📖	mathematical	—	touchpoint reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Finset.map Equiv.toEmbedding Equiv.symm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	orthogonalProjectionSpan_congr range_faceOpposite_reindex excenter_reindex
touchpoint_singleton_mem_interior_faceOpposite 📖	mathematical	—	Set Set.instMembership interior Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.partialOrder faceOpposite touchpoint Finset Finset.instSingleton	—	faceOpposite.eq_1 affineCombination_touchpointWeights affineCombination_mem_interior_face_iff_pos Real.instIsOrderedAddMonoid Nat.AtLeastTwo.neZero_sub_one sum_touchpointWeights touchpointWeights_eq_zero touchpointWeights_singleton_pos

Affine.Simplex.ExcenterExists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineCombination_eq_excenter_iff 📖	mathematical	Affine.Simplex.ExcenterExists Finset.sum Real Real.instAddCommMonoid Finset.univ Fin.fintype Real.instOne	DFunLike.coe AffineMap Real.instRing Pi.addCommGroup 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 Affine.Simplex.points Affine.Simplex.excenter Affine.Simplex.excenterWeights	—	affineIndependent_iff_eq_of_fintype_affineCombination_eq Affine.Simplex.independent sum_excenterWeights_eq_one Affine.Simplex.excenter.eq_1 Affine.Simplex.exsphere.eq_1
affineSpan_faceOpposite_eq_orthRadius 📖	mathematical	Affine.Simplex.ExcenterExists	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range Affine.Simplex.points Affine.Simplex.faceOpposite EuclideanGeometry.Sphere.orthRadius Affine.Simplex.exsphere Affine.Simplex.touchpoint	—	EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eq isTangentAt_touchpoint LT.lt.ne' exradius_pos direction_affineSpan AffineIndependent.finrank_vectorSpan_add_one Affine.Simplex.independent Fintype.card_fin Fact.out
dist_excenter 📖	mathematical	Affine.Simplex.ExcenterExists	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter Affine.Simplex.touchpoint Affine.Simplex.exradius	—	Affine.Simplex.touchpoint.eq_1 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range excenter_mem_affineSpan_range signedInfDist_excenter abs_mul Real.instIsOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Affine.Simplex.exradius_nonneg abs_ite abs_neg abs_one one_mul lt_trichotomy sign_pos Finset.sum_congr Finset.univ_eq_empty sign_neg SignType.coe_neg
dist_excenter_eq_dist_excenter 📖	mathematical	Affine.Simplex.ExcenterExists	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter Affine.Simplex.touchpoint	—	dist_excenter
excenterWeights_eq_excenterWeights_iff 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.excenterWeights Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	sign_eq_sign_or_eq_neg inv_ne_zero Finset.ext sign_mul Real.instIsStrictOrderedRing sign_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_one IsCancelMulZero.toIsLeftCancelMulZero GCDMonoid.toIsCancelMulZero sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike NeZero.one GroupWithZero.toNontrivial neg_mul neg_neg Affine.Simplex.excenterWeights_compl
excenterWeights_ne_zero 📖	—	Affine.Simplex.ExcenterExists	—	—	Affine.Simplex.excenterWeights.eq_1 mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass eq_1 Affine.Simplex.excenterWeightsUnnorm_ne_zero
excenter_eq_excenter_iff 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.excenter Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	—	Affine.Simplex.excenter_eq_affineCombination affineCombination_eq_excenter_iff Affine.Simplex.sum_excenterWeights_eq_one_iff excenterWeights_eq_excenterWeights_iff
excenter_eq_incenter_iff 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.excenter Affine.Simplex.incenter Finset Finset.instEmptyCollection Finset.univ Fin.fintype	—	Affine.Simplex.incenter.eq_1 Affine.Simplex.excenter.eq_1 excenter_eq_excenter_iff Affine.Simplex.excenterExists_empty Finset.compl_empty
excenter_map 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.excenter Affine.Simplex.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 Affine.Simplex.excenterWeights_map Finset.sum_congr Affine.Simplex.excenterWeightsUnnorm_map abs_inv Real.instIsStrictOrderedRing Finset.map_affineCombination sum_excenterWeights_eq_one
excenter_mem_affineSpan_range 📖	mathematical	Affine.Simplex.ExcenterExists	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 Affine.Simplex.points Affine.Simplex.excenter	—	affineCombination_mem_affineSpan Real.instNontrivial sum_excenterWeights_eq_one
excenter_ne_point 📖	—	Affine.Simplex.ExcenterExists	—	—	Finset.card_singleton zero_add excenter_notMem_affineSpan_face Affine.Simplex.face_eq_mkOfPoint Affine.Simplex.range_mkOfPoint_points
excenter_notMem_affineSpan_face 📖	mathematical	Affine.Simplex.ExcenterExists Finset.card	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 Affine.Simplex.points Affine.Simplex.face Affine.Simplex.excenter	—	Eq.ge Fintype.card_fin le_imp_le_of_le_of_le le_refl Finset.card_le_card Finset.subset_univ Finset.exists_mem_notMem_of_card_lt_card excenterWeights_ne_zero AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan Affine.Simplex.independent sum_excenterWeights_eq_one Affine.Simplex.excenter_eq_affineCombination Affine.Simplex.range_face_points Finset.mem_univ
excenter_notMem_affineSpan_faceOpposite 📖	mathematical	Affine.Simplex.ExcenterExists	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 Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.excenter	—	excenter_notMem_affineSpan_face
excenter_notMem_affineSpan_pair 📖	mathematical	Affine.Simplex.ExcenterExists	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 Affine.Simplex.points Set.instSingletonSet Affine.Simplex.excenter	—	Set.insert_eq_of_mem excenter_ne_point Finset.card_insert_of_notMem Finset.card_singleton Affine.Simplex.range_face_points Finset.coe_insert Finset.coe_singleton Set.image_insert_eq Set.image_singleton excenter_notMem_affineSpan_face Nat.AtLeastTwo.ne_one
excenter_restrict 📖	mathematical	Affine.Simplex.ExcenterExists 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 Affine.Simplex.points	SetLike.instMembership AffineSubspace.instSetLike Affine.Simplex.excenter 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 Affine.Simplex.restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective excenter_map Affine.Simplex.excenterExists_restrict
exradius_pos 📖	mathematical	Affine.Simplex.ExcenterExists	Real Real.instLT Real.instZero Affine.Simplex.exradius	—	abs_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inv_ne_zero
isTangentAt_exsphere_iff_eq_touchpoint 📖	mathematical	Affine.Simplex.ExcenterExists	EuclideanGeometry.Sphere.IsTangentAt Affine.Simplex.exsphere affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.touchpoint	—	Affine.Simplex.eq_touchpoint_of_isTangentAt_exsphere isTangentAt_touchpoint
isTangentAt_touchpoint 📖	mathematical	Affine.Simplex.ExcenterExists	EuclideanGeometry.Sphere.IsTangentAt Affine.Simplex.exsphere Affine.Simplex.touchpoint affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.range Affine.Simplex.points Affine.Simplex.faceOpposite	—	Affine.Simplex.touchpoint.eq_1 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.orthogonalProjectionSpan.eq_1 Affine.Simplex.excenter.eq_1 EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt Affine.Simplex.exradius.eq_1 dist_excenter
sOppSide_excenter_point_iff 📖	mathematical	Affine.Simplex.ExcenterExists	AffineSubspace.SOppSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.excenter Real.instLT Affine.Simplex.excenterWeights Real.instZero	—	Real.instIsStrictOrderedRing Affine.Simplex.excenter_eq_affineCombination Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff sum_excenterWeights_eq_one
sOppSide_point_excenter_iff 📖	mathematical	Affine.Simplex.ExcenterExists	AffineSubspace.SOppSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.excenter Real.instLT Affine.Simplex.excenterWeights Real.instZero	—	Real.instIsStrictOrderedRing Affine.Simplex.excenter_eq_affineCombination Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff sum_excenterWeights_eq_one
sSameSide_excenter_point_iff 📖	mathematical	Affine.Simplex.ExcenterExists	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.excenter Real.instLT Real.instZero Affine.Simplex.excenterWeights	—	Real.instIsStrictOrderedRing Affine.Simplex.excenter_eq_affineCombination Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff sum_excenterWeights_eq_one
sSameSide_point_excenter_iff 📖	mathematical	Affine.Simplex.ExcenterExists	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set.range Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.excenter Real.instLT Real.instZero Affine.Simplex.excenterWeights	—	Real.instIsStrictOrderedRing Affine.Simplex.excenter_eq_affineCombination Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff sum_excenterWeights_eq_one
sign_signedInfDist_excenter 📖	mathematical	Affine.Simplex.ExcenterExists	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT ContinuousAffineMap Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike Affine.Simplex.signedInfDist Affine.Simplex.excenter Affine.Simplex.excenterWeights	—	Affine.Simplex.excenter_eq_affineCombination instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.signedInfDist_affineCombination sum_excenterWeights_eq_one sign_mul Real.instIsStrictOrderedRing sign_eq_one_iff dist_eq_norm_vsub Affine.Simplex.height_pos mul_one
sign_signedInfDist_lineMap_excenter_touchpoint 📖	mathematical	Affine.Simplex.ExcenterExists Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	DFunLike.coe OrderHom SignType PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT ContinuousAffineMap Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike Affine.Simplex.signedInfDist AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap Affine.Simplex.excenter Affine.Simplex.touchpoint	—	continuousOn_of_forall_continuousAt ContinuousAt.comp continuousAt_sign_of_ne_zero instOrderTopologyReal touchpoint_notMem_affineSpan_of_ne AffineMap.lineMap_apply_one EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.orthogonalProjectionSpan.eq_1 Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range AffineMap.lineMap_mem excenter_mem_affineSpan_range Affine.Simplex.touchpoint_mem_affineSpan_simplex abs_eq_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add EuclideanGeometry.Sphere.IsTangent.notMem_of_dist_lt EuclideanGeometry.Sphere.IsTangentAt.isTangent isTangentAt_touchpoint dist_lineMap_left dist_excenter IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE exradius_pos abs_lt 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing LE.le.lt_of_ne Continuous.continuousAt Continuous.comp ContinuousAffineMap.cont IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalAddTorsor.toContinuousVAdd instIsTopologicalAddTorsor_1 ContinuousAffineMap.lineMap_toAffineMap IsPreconnected.subsingleton TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologySignType IsConnected.isPreconnected IsConnected.image isConnected_Icc LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono zero_le_one Real.instZeroLEOneClass Set.mem_image_of_mem AffineMap.lineMap_apply_zero Set.left_mem_Icc zero_le_one'
sign_signedInfDist_touchpoint 📖	mathematical	Affine.Simplex.ExcenterExists	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT ContinuousAffineMap Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike Affine.Simplex.signedInfDist Affine.Simplex.touchpoint Affine.Simplex.excenter	—	sign_signedInfDist_lineMap_excenter_touchpoint zero_le_one Real.instZeroLEOneClass le_rfl AffineMap.lineMap_apply_one
sign_touchpointWeights 📖	mathematical	Affine.Simplex.ExcenterExists	DFunLike.coe OrderHom Real SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT Affine.Simplex.touchpointWeights Affine.Simplex.excenterWeights	—	sign_signedInfDist_touchpoint instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.signedInfDist_affineCombination Affine.Simplex.sum_touchpointWeights sign_signedInfDist_excenter Affine.Simplex.affineCombination_touchpointWeights sign_mul Real.instIsStrictOrderedRing sign_eq_one_iff dist_eq_norm_vsub Affine.Simplex.height_pos mul_one
signedInfDist_excenter 📖	mathematical	Affine.Simplex.ExcenterExists	DFunLike.coe ContinuousAffineMap Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike Affine.Simplex.signedInfDist Affine.Simplex.excenter Real.instMul Finset Finset.instMembership Finset.decidableMem Real.instNeg Real.instOne SignType.cast Real.instZero OrderHom SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT Finset.sum Real.instAddCommMonoid Finset.univ Fin.fintype Affine.Simplex.excenterWeightsUnnorm Affine.Simplex.exradius	—	signedInfDist_excenter_eq_mul_sum_inv mul_assoc Affine.Simplex.exradius_eq_abs_inv_sum mul_eq_one_iff_inv_eq₀ self_mul_sign Real.instIsStrictOrderedRing abs_mul Real.instIsOrderedRing mul_inv_cancel₀ abs_one
signedInfDist_excenter_eq_mul_sum_inv 📖	mathematical	Affine.Simplex.ExcenterExists	DFunLike.coe ContinuousAffineMap Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedAddTorsor.toAddTorsor Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor ContinuousAffineMap.instFunLike Affine.Simplex.signedInfDist Affine.Simplex.excenter Real.instMul Finset Finset.instMembership Finset.decidableMem Real.instNeg Real.instOne Real.instInv Finset.sum Real.instAddCommMonoid Finset.univ Fin.fintype Affine.Simplex.excenterWeightsUnnorm	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.signedInfDist_affineCombination sum_excenterWeights_eq_one Finset.sum_congr Affine.Simplex.altitudeFoot.eq_1 Affine.Simplex.height.eq_1 ite_mul neg_mul one_mul mul_ite mul_neg inv_mul_cancel_right₀ LT.lt.ne' Affine.Simplex.height_pos
sum_excenterWeights_eq_one 📖	mathematical	Affine.Simplex.ExcenterExists	Finset.sum Real Real.instAddCommMonoid Finset.univ Fin.fintype Affine.Simplex.excenterWeights Real.instOne	—	Affine.Simplex.sum_excenterWeights_eq_one_iff
touchpointWeights_map 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.touchpointWeights Affine.Simplex.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 Affine.Simplex.affineCombination_eq_touchpoint_iff Affine.Simplex.sum_touchpointWeights Affine.Simplex.affineCombination_touchpointWeights AffineIsometry.map_eq_iff AffineIsometry.coe_toAffineMap Finset.map_affineCombination Affine.Simplex.map_points touchpoint_map
touchpointWeights_restrict 📖	mathematical	Affine.Simplex.ExcenterExists 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 Affine.Simplex.points	Affine.Simplex.touchpointWeights 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 Affine.Simplex.restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective touchpointWeights_map Affine.Simplex.excenterExists_restrict
touchpoint_injective 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.touchpoint	—	AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent Affine.Simplex.touchpoint_eq_point_rev Fin.exists_ne_and_ne_of_two_lt Affine.Simplex.range_faceOpposite_points Set.inter_singleton_of_notMem Set.compl_empty Set.image_univ AffineSubspace.vectorSpan_union_of_mem_of_mem Set.mem_image_of_mem Submodule.inf_orthogonal direction_affineSpan EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal AffineSubspace.vsub_mem_direction excenter_mem_affineSpan_range Affine.Simplex.touchpoint_mem_affineSpan_simplex Submodule.mem_bot Submodule.inf_orthogonal_eq_bot LT.lt.ne' exradius_pos dist_excenter dist_eq_norm_vsub norm_eq_zero
touchpoint_map 📖	mathematical	Affine.Simplex.ExcenterExists	Affine.Simplex.touchpoint Affine.Simplex.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 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange excenter_map
touchpoint_mem_exsphere 📖	mathematical	Affine.Simplex.ExcenterExists	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Affine.Simplex.exsphere Affine.Simplex.touchpoint	—	EuclideanGeometry.mem_sphere' dist_excenter
touchpoint_ne_point 📖	—	Affine.Simplex.ExcenterExists	—	—	Nat.AtLeastTwo.one_lt Fin.exists_ne_and_ne_of_two_lt Affine.Simplex.affineCombination_eq_touchpoint_iff Finset.sum_affineCombinationSingleWeights Finset.mem_univ Finset.affineCombination_affineCombinationSingleWeights neg_mul one_mul LT.lt.ne' Affine.Simplex.height_pos Affine.Simplex.excenterWeightsUnnorm.eq_1 sign_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass eq_1 Affine.Simplex.excenterWeights.eq_1 sign_touchpointWeights Finset.affineCombinationSingleWeights_apply_of_ne
touchpoint_notMem_affineSpan_of_ne 📖	mathematical	Affine.Simplex.ExcenterExists	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 Affine.Simplex.points Affine.Simplex.faceOpposite Affine.Simplex.touchpoint	—	touchpoint_injective EuclideanGeometry.Sphere.IsTangentAt.eq_of_mem_of_mem isTangentAt_touchpoint touchpoint_mem_exsphere
touchpoint_restrict 📖	mathematical	Affine.Simplex.ExcenterExists 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 Affine.Simplex.points	SetLike.instMembership AffineSubspace.instSetLike Affine.Simplex.touchpoint 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 Affine.Simplex.restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective touchpoint_map Affine.Simplex.excenterExists_restrict

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_pair_eq_orthRadius 📖	mathematical	—	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Affine.Simplex.points Set.instSingletonSet EuclideanGeometry.Sphere.orthRadius Affine.Simplex.exsphere Affine.Simplex.touchpoint	—	Affine.Simplex.range_faceOpposite_points Set.image_insert_eq Set.image_singleton Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius excenterExists
affineSpan_pair_eq_orthRadius_insphere 📖	mathematical	—	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Affine.Simplex.points Set.instSingletonSet EuclideanGeometry.Sphere.orthRadius Affine.Simplex.insphere Affine.Simplex.touchpoint Finset Finset.instEmptyCollection	—	affineSpan_pair_eq_orthRadius
excenterExists 📖	mathematical	—	Affine.Simplex.ExcenterExists	—	Affine.Simplex.excenterExists_empty Affine.Simplex.excenterExists_compl Affine.Simplex.excenterExists_singleton Nat.instAtLeastTwoHAddOfNat
excenter_eq_incenter_or_excenter_singleton 📖	mathematical	—	Affine.Simplex.excenter Affine.Simplex.incenter Finset Finset.instSingleton	—	Affine.Simplex.excenter_univ Affine.Simplex.excenter_compl
excenter_eq_incenter_or_excenter_singleton_of_ne 📖	mathematical	—	Affine.Simplex.excenter Affine.Simplex.incenter Finset Finset.instSingleton	—	excenter_eq_incenter_or_excenter_singleton
sOppSide_affineSpan_pair_excenter_singleton_point 📖	mathematical	—	AffineSubspace.SOppSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set Set.instInsert Affine.Simplex.points Set.instSingletonSet Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing Affine.Simplex.range_faceOpposite_points Affine.Simplex.sOppSide_excenter_singleton_point Nat.instAtLeastTwoHAddOfNat
sOppSide_affineSpan_pair_point_excenter_singleton 📖	mathematical	—	AffineSubspace.SOppSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set Set.instInsert Affine.Simplex.points Set.instSingletonSet Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing Affine.Simplex.range_faceOpposite_points Affine.Simplex.sOppSide_point_excenter_singleton Nat.instAtLeastTwoHAddOfNat
sSameSide_affineSpan_pair_excenter_singleton_point 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set Set.instInsert Affine.Simplex.points Set.instSingletonSet Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing Affine.Simplex.range_faceOpposite_points Affine.Simplex.sSameSide_excenter_singleton_point Nat.instAtLeastTwoHAddOfNat
sSameSide_affineSpan_pair_incenter_point 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set Set.instInsert Affine.Simplex.points Set.instSingletonSet Affine.Simplex.incenter	—	Real.instIsStrictOrderedRing Affine.Simplex.range_faceOpposite_points Affine.Simplex.sSameSide_incenter_point
sSameSide_affineSpan_pair_point_excenter_singleton 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set Set.instInsert Affine.Simplex.points Set.instSingletonSet Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing Affine.Simplex.range_faceOpposite_points Affine.Simplex.sSameSide_point_excenter_singleton Nat.instAtLeastTwoHAddOfNat
sSameSide_affineSpan_pair_point_incenter 📖	mathematical	—	AffineSubspace.SSameSide Real Real.commRing Real.partialOrder Real.instIsStrictOrderedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace affineSpan Real.instRing Set Set.instInsert Affine.Simplex.points Set.instSingletonSet Affine.Simplex.incenter	—	Real.instIsStrictOrderedRing Affine.Simplex.range_faceOpposite_points Affine.Simplex.sSameSide_point_incenter
sbtw_touchpoint_empty 📖	mathematical	—	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.points Affine.Simplex.touchpoint Finset Finset.instEmptyCollection	—	Finset.card_pair Affine.Simplex.mem_interior_face_iff_sbtw Real.instIsOrderedRing Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Affine.Simplex.faceOpposite.eq_1 Affine.Simplex.touchpoint_empty_mem_interior_faceOpposite Nat.instAtLeastTwoHAddOfNat
sbtw_touchpoint_singleton 📖	mathematical	—	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.points Affine.Simplex.touchpoint Finset Finset.instSingleton	—	Finset.card_pair Affine.Simplex.mem_interior_face_iff_sbtw Real.instIsOrderedRing Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Affine.Simplex.faceOpposite.eq_1 Affine.Simplex.touchpoint_singleton_mem_interior_faceOpposite Nat.instAtLeastTwoHAddOfNat
touchpoint_singleton_sbtw 📖	mathematical	—	Sbtw Real Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.touchpoint Finset Finset.instSingleton Affine.Simplex.points	—	Affine.Simplex.affineCombination_touchpointWeights Affine.Simplex.sum_touchpointWeights Finset.affineCombinationLineMapWeights_apply_left add_sub_cancel_right Finset.sum_congr Finset.sum_insert Affine.Simplex.touchpointWeights_eq_zero Finset.sum_singleton zero_add Finset.affineCombinationLineMapWeights_apply_of_ne Finset.affineCombinationLineMapWeights_apply_right Finset.affineCombination_affineCombinationLineMapWeights Finset.mem_univ sbtw_iff_right_ne_and_left_mem_image_Ioi Real.instIsStrictOrderedRing AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Affine.Simplex.touchpointWeights_singleton_neg Nat.instAtLeastTwoHAddOfNat

---

← Back to Index