Incenter

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

Statistics

Metric	Count
Definitions	0
Theorems angle_excenter_touchpoint_eq, angle_incenter_touchpoint_eq, exists_excenterExists_and_eq_excenter_of_forall_angle_orthogonalProjectionSpan_eq, dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq, eq_excenter_of_two_zsmul_oangle_eq, eq_excenter_singleton_of_oangle_eq_add_pi, eq_excenter_singleton_of_oangle_eq_add_pi_of_oangle_eq_add_pi, eq_excenter_singleton_of_oangle_eq_of_oangle_eq_add_pi, eq_incenter_of_oangle_eq, eq_incenter_or_eq_excenter_singleton_of_oangle_eq, oangle_excenter_singleton_eq, oangle_excenter_singleton_eq_add_pi, oangle_incenter_eq, two_zsmul_oangle_excenter_eq	14
Total	14

Affine.Simplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_incenter_touchpoint_eq 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite	EuclideanGeometry.angle incenter touchpoint Finset Finset.instEmptyCollection	—	ExcenterExists.angle_excenter_touchpoint_eq excenterExists_empty
exists_excenterExists_and_eq_excenter_of_forall_angle_orthogonalProjectionSpan_eq 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite EuclideanGeometry.angle NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan	Finset ExcenterExists excenter	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Finite.of_fintype EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq

Affine.Simplex.ExcenterExists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angle_excenter_touchpoint_eq 📖	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	EuclideanGeometry.angle Affine.Simplex.excenter Affine.Simplex.touchpoint	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_range Finite.of_fintype EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq dist_excenter_eq_dist_excenter

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace AffineSubspace Real NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range Affine.Simplex.points Affine.Simplex.faceOpposite Real.instRing Real.normedField DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike Affine.Simplex.orthogonalProjectionSpan Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle	—	Real.instIsStrictOrderedRing Fintype.complete Fin.instNeZeroHAddNatOfNat_mathlib_1 AffineIndependent.comp_embedding Affine.Simplex.independent instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Affine.Simplex.orthogonalProjectionSpan.eq_1 Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_insert_set finiteDimensional_direction_affineSpan_singleton EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq Affine.Simplex.range_faceOpposite_points EuclideanGeometry.orthogonalProjection_congr Set.image_insert_eq Set.image_singleton
eq_excenter_of_two_zsmul_oangle_eq 📖	mathematical	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Finset Affine.Simplex.excenter	—	Real.instIsStrictOrderedRing AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one FiniteDimensional.of_fact_finrank_eq_two Affine.Simplex.independent Fintype.card_fin Fact.out AffineSubspace.mem_top instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter
eq_excenter_singleton_of_oangle_eq_add_pi 📖	mathematical	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing excenter_eq_incenter_or_excenter_singleton_of_ne AddLeftCancelSemigroup.toIsLeftCancelAdd oangle_incenter_eq oangle_excenter_singleton_eq
eq_excenter_singleton_of_oangle_eq_add_pi_of_oangle_eq_add_pi 📖	mathematical	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing eq_excenter_of_two_zsmul_oangle_eq smul_add Real.Angle.two_zsmul_coe_pi add_zero eq_excenter_singleton_of_oangle_eq_add_pi Affine.Simplex.excenter_singleton_injective Nat.instAtLeastTwoHAddOfNat
eq_excenter_singleton_of_oangle_eq_of_oangle_eq_add_pi 📖	mathematical	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing eq_excenter_of_two_zsmul_oangle_eq smul_add Real.Angle.two_zsmul_coe_pi add_zero eq_incenter_or_eq_excenter_singleton_of_oangle_eq eq_excenter_singleton_of_oangle_eq_add_pi Affine.Simplex.excenter_singleton_ne_incenter Nat.instAtLeastTwoHAddOfNat
eq_incenter_of_oangle_eq 📖	mathematical	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Affine.Simplex.incenter	—	Real.instIsStrictOrderedRing eq_excenter_of_two_zsmul_oangle_eq eq_incenter_or_eq_excenter_singleton_of_oangle_eq Affine.Simplex.excenter_singleton_injective Nat.instAtLeastTwoHAddOfNat
eq_incenter_or_eq_excenter_singleton_of_oangle_eq 📖	mathematical	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter	Affine.Simplex.excenter Affine.Simplex.incenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing excenter_eq_incenter_or_excenter_singleton_of_ne AddLeftCancelSemigroup.toIsLeftCancelAdd oangle_excenter_singleton_eq_add_pi neg_add_rev Real.Angle.neg_coe_pi AddRightCancelSemigroup.toIsRightCancelAdd EuclideanGeometry.oangle_rev
oangle_excenter_singleton_eq 📖	mathematical	—	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter Finset Finset.instSingleton	—	Real.instIsStrictOrderedRing Sbtw.oangle_eq_left Sbtw.symm Real.instIsOrderedRing touchpoint_singleton_sbtw Sbtw.oangle_eq_right Affine.Simplex.ExcenterExists.dist_excenter_eq_dist_excenter Affine.Simplex.excenterExists_singleton Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq mem_affineSpan Affine.Simplex.range_faceOpposite_points Affine.Simplex.ExcenterExists.touchpoint_injective
oangle_excenter_singleton_eq_add_pi 📖	mathematical	—	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter Finset Finset.instSingleton Real.Angle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instNormedAddCommGroupAngle ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.Angle.coe Real.pi	—	Real.instIsStrictOrderedRing Sbtw.oangle_eq_add_pi_left Sbtw.symm Real.instIsOrderedRing touchpoint_singleton_sbtw Affine.Simplex.ExcenterExists.excenter_ne_point Affine.Simplex.excenterExists_singleton Nat.instAtLeastTwoHAddOfNat Sbtw.oangle_eq_right sbtw_touchpoint_singleton AddRightCancelSemigroup.toIsRightCancelAdd Affine.Simplex.ExcenterExists.dist_excenter_eq_dist_excenter EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq mem_affineSpan Affine.Simplex.range_faceOpposite_points Affine.Simplex.ExcenterExists.touchpoint_injective
oangle_incenter_eq 📖	mathematical	—	EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.incenter	—	Real.instIsStrictOrderedRing Sbtw.oangle_eq_left sbtw_touchpoint_empty Sbtw.oangle_eq_right Affine.Simplex.dist_incenter_eq_dist_incenter EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq mem_affineSpan Affine.Simplex.range_faceOpposite_points Affine.Simplex.touchpoint_empty_injective
two_zsmul_oangle_excenter_eq 📖	mathematical	—	Real.Angle SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instNormedAddCommGroupAngle EuclideanGeometry.oangle Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Simplex.excenter	—	Real.instIsStrictOrderedRing instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq Affine.Simplex.touchpoint.eq_1 Affine.Simplex.ExcenterExists.dist_excenter_eq_dist_excenter excenterExists

---

← Back to Index