MongePoint

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

Statistics

Metric	Count
Definitions mongePlane, mongePoint, mongePointVSubFaceCentroidWeightsWithCircumcenter, mongePointWeightsWithCircumcenter, orthocenter, OrthocentricSystem	6
Theorems direction_mongePlane, eq_mongePoint_of_forall_mem_mongePlane, inner_mongePoint_vsub_face_centroid_vsub, mongePlane_comm, mongePlane_def, mongePlane_reindex, mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, mongePoint_eq_affineCombination_of_pointsWithCircumcenter, mongePoint_eq_of_range_eq, mongePoint_eq_smul_vsub_vadd_circumcenter, mongePoint_map, mongePoint_mem_affineSpan, mongePoint_mem_mongePlane, mongePoint_reindex, mongePoint_restrict, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, smul_mongePoint_vsub_circumcenter_eq_sum_vsub, sum_mongePointVSubFaceCentroidWeightsWithCircumcenter, sum_mongePointWeightsWithCircumcenter, affineSpan_orthocenter_point_le_altitude, altitude_eq_mongePlane, altitude_replace_orthocenter_eq_affineSpan, dist_circumcenter_reflection_orthocenter, dist_circumcenter_reflection_orthocenter_finset, dist_orthocenter_reflection_circumcenter, dist_orthocenter_reflection_circumcenter_finset, eq_orthocenter_of_forall_mem_altitude, orthocenter_eq_mongePoint, orthocenter_eq_of_range_eq, orthocenter_eq_smul_vsub_vadd_circumcenter, orthocenter_mem_affineSpan, orthocenter_mem_altitude, orthocenter_reindex, orthocenter_replace_orthocenter_eq_point, orthocenter_vsub_circumcenter_eq_sum_vsub, affineIndependent, eq_insert_orthocenter, exists_circumradius_eq, affineSpan_of_orthocentricSystem, exists_dist_eq_circumradius_of_subset_insert_orthocenter, exists_of_range_subset_orthocentricSystem	41
Total	47

Affine.Simplex

Definitions

Name	Category	Theorems
mongePlane 📖	CompOp	6 math math: mongePoint_mem_mongePlane, mongePlane_def, direction_mongePlane, mongePlane_reindex, Affine.Triangle.altitude_eq_mongePlane, mongePlane_comm
mongePoint 📖	CompOp	14 math math: smul_mongePoint_vsub_circumcenter_eq_sum_vsub, mongePoint_eq_of_range_eq, mongePoint_mem_mongePlane, inner_mongePoint_vsub_face_centroid_vsub, mongePoint_eq_affineCombination_of_pointsWithCircumcenter, mongePoint_reindex, mongePoint_eq_smul_vsub_vadd_circumcenter, eq_mongePoint_of_forall_mem_mongePlane, mongePoint_restrict, mongePoint_map, mongePoint_mem_affineSpan, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, Affine.Triangle.orthocenter_eq_mongePoint, points_vsub_eulerPoint
mongePointVSubFaceCentroidWeightsWithCircumcenter 📖	CompOp	3 math math: mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, sum_mongePointVSubFaceCentroidWeightsWithCircumcenter, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter
mongePointWeightsWithCircumcenter 📖	CompOp	3 math math: mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, sum_mongePointWeightsWithCircumcenter, mongePoint_eq_affineCombination_of_pointsWithCircumcenter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
direction_mongePlane 📖	mathematical	—	AffineSubspace.direction Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace mongePlane Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.instMin Submodule.orthogonal Submodule.span Real.semiring Set Set.instSingletonSet VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup points vectorSpan SeminormedAddCommGroup.toAddCommGroup Set.range	—	mongePlane_def AffineSubspace.direction_inf_of_mem_inf mongePoint_mem_mongePlane AffineSubspace.direction_mk' direction_affineSpan
eq_mongePoint_of_forall_mem_mongePlane 📖	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 mongePlane	mongePoint	—	vsub_eq_zero_iff_eq direction_mongePlane AffineSubspace.vsub_right_mem_direction_iff_mem mongePoint_mem_mongePlane Submodule.mem_iInf Submodule.mem_inf Set.image_image Set.ext Set.mem_univ Finset.card_pos Finset.card_erase_of_mem Fintype.card_fin IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat Finset.ne_of_mem_erase Submodule.disjoint_def Submodule.orthogonal_disjoint Set.image_univ vectorSpan_image_eq_span_vsub_set_left_ne Submodule.span_iUnion Submodule.iInf_orthogonal
inner_mongePoint_vsub_face_centroid_vsub 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace mongePoint Finset.centroid Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instInsert Finset.instSingleton points Real.instRing Real.instZero	—	Finset.insert_eq_of_mem vsub_self inner_zero_right mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter point_eq_affineCombination_of_pointsWithCircumcenter Finset.affineCombination_vsub Finset.sum_congr Finset.sum_sub_distrib sum_pointWeightsWithCircumcenter sub_self Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.inner_weightedVSub sum_mongePointVSubFaceCentroidWeightsWithCircumcenter sum_pointsWithCircumcenter pointsWithCircumcenter_eq_circumcenter Finset.sum_subset Finset.subset_univ MulZeroClass.zero_mul Finset.sum_const_zero Nat.cast_add Nat.cast_one MulZeroClass.mul_zero dist_circumcenter_eq_circumradius' Finset.sum_insert Finset.notMem_singleton Finset.sum_singleton sub_zero mul_one dist_self zero_sub mul_neg dist_comm neg_mul zero_add add_zero dist_circumcenter_eq_circumradius neg_add_cancel add_neg_cancel neg_zero zero_div
mongePlane_comm 📖	mathematical	—	mongePlane	—	Finset.pair_comm Submodule.ext neg_smul smul_neg neg_vsub_eq_vsub_rev
mongePlane_def 📖	mathematical	—	mongePlane AffineSubspace Real CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AffineSubspace.instCompleteLattice AffineSubspace.mk' Finset.centroid Real.instDivisionRing NormedAddCommGroup.toAddCommGroup Real.normedField Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instInsert Finset.instSingleton points Real.instRing Submodule.orthogonal Submodule.span Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set Set.instSingletonSet VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup affineSpan Set.range	—	—
mongePlane_reindex 📖	mathematical	—	mongePlane reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Fintype.card_fin Fintype.card_eq reindex_range_points Finset.ext Finset.compl_insert Finset.map_erase Equiv.apply_symm_apply EquivLike.toEmbeddingLike Equiv.symm_comp_self CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Finset.card_compl Finset.insert_eq_of_mem Finset.card_singleton Finset.card_insert_of_notMem Finset.affineCombination_map
mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub 📖	mathematical	—	mongePointVSubFaceCentroidWeightsWithCircumcenter Pi.instSub PointsWithCircumcenterIndex Real Real.instSub mongePointWeightsWithCircumcenter centroidWeightsWithCircumcenter Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instInsert Finset.instSingleton	—	Pi.sub_apply mongePointWeightsWithCircumcenter.eq_1 centroidWeightsWithCircumcenter.eq_1 mongePointVSubFaceCentroidWeightsWithCircumcenter.eq_1 Finset.compl_insert Finset.card_erase_of_mem Finset.card_compl Fintype.card_fin Finset.card_singleton Nat.cast_add Nat.cast_one sub_zero sub_self
mongePoint_eq_affineCombination_of_pointsWithCircumcenter 📖	mathematical	—	mongePoint DFunLike.coe AffineMap Real Real.instRing Pi.addCommGroup PointsWithCircumcenterIndex Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike Finset.affineCombination Finset.univ instFintypePointsWithCircumcenterIndex pointsWithCircumcenter mongePointWeightsWithCircumcenter	—	mongePoint_eq_smul_vsub_vadd_circumcenter centroid_eq_affineCombination_of_pointsWithCircumcenter circumcenter_eq_affineCombination_of_pointsWithCircumcenter Finset.affineCombination_vsub map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Finset.weightedVSub_vadd_affineCombination Pi.add_apply Pi.smul_apply smul_eq_mul Pi.sub_apply add_tsub_assoc_of_le StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Finset.mem_univ Finset.card_fin Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Nat.cast_pos' Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike add_pos' Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Nat.instAtLeastTwoHAddOfNat Nat.cast_add zero_sub mul_neg Mathlib.Tactic.FieldSimp.NF.one_eq_eval Nat.cast_nonneg' Real.instIsOrderedRing Real.instNontrivial neg_div neg_add_rev Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat
mongePoint_eq_of_range_eq 📖	mathematical	Set.range points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	mongePoint	—	centroid_eq_of_range_eq circumcenter_eq_of_range_eq
mongePoint_eq_smul_vsub_vadd_circumcenter 📖	mathematical	—	mongePoint HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Finset.centroid Real.instDivisionRing NormedAddCommGroup.toAddCommGroup Finset.univ Fin.fintype points Real.instRing circumcenter	—	—
mongePoint_map 📖	mathematical	—	mongePoint 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 centroid.eq_1 Nat.cast_add Nat.cast_one centroid_map RCLike.charZero_rclike AffineIsometry.coe_toAffineMap circumcenter_map AffineIsometry.map_vadd map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass LinearIsometry.instSemilinearIsometryClass AffineIsometry.map_vsub
mongePoint_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 mongePoint	—	AffineSubspace.smul_vsub_vadd_mem centroid_mem_affineSpan_of_card_eq_add_one RCLike.charZero_rclike Finset.card_fin circumcenter_mem_affineSpan
mongePoint_mem_mongePlane 📖	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 mongePlane mongePoint	—	mongePlane_def AffineSubspace.mem_inf_iff AffineSubspace.vsub_right_mem_direction_iff_mem AffineSubspace.self_mem_mk' AffineSubspace.direction_mk' Submodule.mem_orthogonal' Submodule.mem_span_singleton inner_smul_right inner_mongePoint_vsub_face_centroid_vsub MulZeroClass.mul_zero mongePoint_mem_affineSpan
mongePoint_reindex 📖	mathematical	—	mongePoint reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	circumcenter_reindex Fintype.card_fin Fintype.card_eq Finset.univ_map_embedding Equiv.symm_comp_self CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Finset.affineCombination_map
mongePoint_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 mongePoint Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor Nonempty.map DFunLike.coe AffineMap Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange centroid.eq_1 Nat.cast_add Nat.cast_one centroid_restrict RCLike.charZero_rclike circumcenter_restrict
mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter 📖	mathematical	—	VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace mongePoint Finset.centroid Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instInsert Finset.instSingleton points Real.instRing DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid PointsWithCircumcenterIndex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike Finset.weightedVSub Finset.univ instFintypePointsWithCircumcenterIndex pointsWithCircumcenter mongePointVSubFaceCentroidWeightsWithCircumcenter	—	mongePoint_eq_affineCombination_of_pointsWithCircumcenter centroid_eq_affineCombination_of_pointsWithCircumcenter Finset.affineCombination_vsub mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub
smul_mongePoint_vsub_circumcenter_eq_sum_vsub 📖	mathematical	—	AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace mongePoint circumcenter Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid Finset.univ Fin.fintype points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	mongePoint_eq_smul_vsub_vadd_circumcenter vadd_vsub smul_assoc AddCommMonoid.nat_isScalarTower Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_one nsmul_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat RCLike.charZero_rclike smul_eq_iff_eq_invOf_smul Finset.smul_sum univ_centroid_eq centroid_eq_affineCombination Finset.sum_smul_vsub_const_eq_affineCombination_vsub Finset.sum_congr Fintype.card_fin Finset.sum_const mul_inv_cancel_of_invertible invOf_eq_inv
sum_mongePointVSubFaceCentroidWeightsWithCircumcenter 📖	mathematical	—	Finset.sum PointsWithCircumcenterIndex Real Real.instAddCommMonoid Finset.univ instFintypePointsWithCircumcenterIndex mongePointVSubFaceCentroidWeightsWithCircumcenter Real.instZero	—	mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub Finset.sum_congr Finset.sum_sub_distrib sum_mongePointWeightsWithCircumcenter sum_centroidWeightsWithCircumcenter Finset.compl_insert Finset.card_erase_of_mem Finset.card_compl Fintype.card_fin Finset.card_singleton add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd sub_self
sum_mongePointWeightsWithCircumcenter 📖	mathematical	—	Finset.sum PointsWithCircumcenterIndex Real Real.instAddCommMonoid Finset.univ instFintypePointsWithCircumcenterIndex mongePointWeightsWithCircumcenter Real.instOne	—	sum_pointsWithCircumcenter Finset.sum_congr Finset.sum_const Finset.card_fin nsmul_eq_mul Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ mul_neg Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add

Affine.Triangle

Definitions

Name	Category	Theorems
orthocenter 📖	CompOp	15 math math: orthocenter_eq_smul_vsub_vadd_circumcenter, orthocenter_eq_of_range_eq, dist_circumcenter_reflection_orthocenter, dist_orthocenter_reflection_circumcenter, affineSpan_orthocenter_point_le_altitude, orthocenter_mem_altitude, eulerPoint_eq_midpoint, dist_circumcenter_reflection_orthocenter_finset, EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter, orthocenter_mem_affineSpan, orthocenter_eq_mongePoint, eq_orthocenter_of_forall_mem_altitude, orthocenter_vsub_circumcenter_eq_sum_vsub, dist_orthocenter_reflection_circumcenter_finset, orthocenter_reindex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_orthocenter_point_le_altitude 📖	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 Set.instInsert orthocenter Set.instSingletonSet Affine.Simplex.points Affine.Simplex.altitude	—	affineSpan_le_of_subset_coe Set.insert_subset_iff Set.singleton_subset_iff orthocenter_mem_altitude Affine.Simplex.mem_altitude
altitude_eq_mongePlane 📖	mathematical	—	Affine.Simplex.altitude Affine.Simplex.mongePlane	—	Affine.Simplex.mongePlane_def Affine.Simplex.altitude_def direction_affineSpan Finset.centroid_singleton vectorSpan_image_eq_span_vsub_set_left_ne Set.mem_insert Set.insert_diff_of_mem Set.diff_singleton_eq_self Set.image_singleton
altitude_replace_orthocenter_eq_affineSpan 📖	mathematical	Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthocenter	Affine.Simplex.altitude affineSpan Set Set.instInsert Set.instSingletonSet	—	Affine.Simplex.affineSpan_pair_eq_altitude_iff AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent AffineSubspace.ext_of_direction_eq Submodule.eq_of_le_of_finrank_eq finiteDimensional_direction_affineSpan_range Finite.of_fintype AffineSubspace.direction_le affineSpan_le_of_subset_coe Set.image_univ Set.image_insert_eq Set.image_singleton Set.insert_subset_iff Set.singleton_subset_iff orthocenter_mem_affineSpan mem_affineSpan Set.mem_range_self direction_affineSpan AffineIndependent.finrank_vectorSpan Fintype.card_fin Submodule.orthogonal_le affineSpan_orthocenter_point_le_altitude Affine.Simplex.vectorSpan_isOrtho_altitude_direction vsub_mem_vectorSpan Set.mem_insert Set.mem_insert_of_mem Set.mem_singleton
dist_circumcenter_reflection_orthocenter 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.circumcenter DFunLike.coe AffineIsometryEquiv Real DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike EuclideanGeometry.reflection affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor Set.image Affine.Simplex.points Real.normedField Set Set.instInsert Set.instSingletonSet instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing complete_of_proper Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Real.instDivisionRing Finite.of_fintype Fin.fintype orthocenter Affine.Simplex.circumradius	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Finite.of_fintype EuclideanGeometry.dist_reflection dist_comm dist_orthocenter_reflection_circumcenter
dist_circumcenter_reflection_orthocenter_finset 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.circumcenter DFunLike.coe AffineIsometryEquiv Real DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike EuclideanGeometry.reflection affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor Set.image Affine.Simplex.points Real.normedField SetLike.coe Finset Finset.instSetLike Finset.instInsert Finset.instSingleton instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Finset.instNonemptyElemCoeInsert Submodule.HasOrthogonalProjection.ofCompleteSpace AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing complete_of_proper Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Real.instDivisionRing Finite.of_fintype Fin.fintype orthocenter Affine.Simplex.circumradius	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Finset.instNonemptyElemCoeInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Finite.of_fintype Finset.coe_insert Finset.coe_singleton EuclideanGeometry.reflection.congr_simp dist_circumcenter_reflection_orthocenter
dist_orthocenter_reflection_circumcenter 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace orthocenter DFunLike.coe AffineIsometryEquiv Real DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike EuclideanGeometry.reflection affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor Set.image Affine.Simplex.points Real.normedField Set Set.instInsert Set.instSingletonSet instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing complete_of_proper Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Real.instDivisionRing Finite.of_fintype Fin.fintype Affine.Simplex.circumcenter Affine.Simplex.circumradius	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Finite.of_fintype mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing dist_nonneg Affine.Simplex.circumradius_nonneg Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter orthocenter_eq_mongePoint Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.dist_affineCombination Affine.Simplex.sum_mongePointWeightsWithCircumcenter Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter Finset.sum_congr Affine.Simplex.sum_pointsWithCircumcenter Finset.subset_univ Finset.sum_sdiff Mathlib.Meta.NormNum.IsNat.to_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_natCast Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Finset.sum_singleton sub_zero mul_one Finset.sum_insert_of_eq_zero_if_notMem sub_self MulZeroClass.mul_zero MulZeroClass.zero_mul add_zero Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.instAtLeastTwo mul_neg neg_sub Affine.Simplex.dist_circumcenter_eq_circumradius dist_self zero_sub neg_mul one_mul zero_add Affine.Simplex.dist_circumcenter_eq_circumradius' Mathlib.Meta.NormNum.IsInt.to_isNat neg_add_rev neg_neg add_self_div_two CharZero.NeZero.two
dist_orthocenter_reflection_circumcenter_finset 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace orthocenter DFunLike.coe AffineIsometryEquiv Real DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike EuclideanGeometry.reflection affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor Set.image Affine.Simplex.points Real.normedField SetLike.coe Finset Finset.instSetLike Finset.instInsert Finset.instSingleton instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Finset.instNonemptyElemCoeInsert Submodule.HasOrthogonalProjection.ofCompleteSpace AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing complete_of_proper Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Real.instDivisionRing Finite.of_fintype Fin.fintype Affine.Simplex.circumcenter Affine.Simplex.circumradius	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Finset.instNonemptyElemCoeInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Finite.of_fintype Finset.coe_insert Finset.coe_singleton EuclideanGeometry.reflection.congr_simp dist_orthocenter_reflection_circumcenter
eq_orthocenter_of_forall_mem_altitude 📖	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 Affine.Simplex.altitude	orthocenter	—	orthocenter_eq_mongePoint altitude_eq_mongePlane Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane
orthocenter_eq_mongePoint 📖	mathematical	—	orthocenter Affine.Simplex.mongePoint	—	—
orthocenter_eq_of_range_eq 📖	mathematical	Set.range Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	orthocenter	—	Affine.Simplex.mongePoint_eq_of_range_eq
orthocenter_eq_smul_vsub_vadd_circumcenter 📖	mathematical	—	orthocenter HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Finset.centroid Real.instDivisionRing NormedAddCommGroup.toAddCommGroup Finset.univ Fin.fintype Affine.Simplex.points Real.instRing Affine.Simplex.circumcenter	—	Nat.instAtLeastTwoHAddOfNat orthocenter_eq_mongePoint Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter Nat.cast_one div_one
orthocenter_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 Affine.Simplex.points orthocenter	—	Affine.Simplex.mongePoint_mem_affineSpan
orthocenter_mem_altitude 📖	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 Affine.Simplex.altitude orthocenter	—	orthocenter_eq_mongePoint altitude_eq_mongePlane Affine.Simplex.mongePoint_mem_mongePlane
orthocenter_reindex 📖	mathematical	—	orthocenter Affine.Simplex.reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	Affine.Simplex.mongePoint_reindex
orthocenter_replace_orthocenter_eq_point 📖	—	Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthocenter	—	—	eq_orthocenter_of_forall_mem_altitude altitude_replace_orthocenter_eq_affineSpan mem_affineSpan Set.mem_insert
orthocenter_vsub_circumcenter_eq_sum_vsub 📖	mathematical	—	VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace orthocenter Affine.Simplex.circumcenter Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.univ Fin.fintype Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub zero_add one_smul orthocenter_eq_mongePoint

EuclideanGeometry

Definitions

Name	Category	Theorems
OrthocentricSystem 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_of_orthocentricSystem 📖	mathematical	OrthocentricSystem Set Set.instHasSubset Set.range	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	OrthocentricSystem.affineIndependent affineSpan_insert_eq_affineSpan Affine.Triangle.orthocenter_mem_affineSpan AffineSubspace.ext_of_direction_eq finiteDimensional_direction_affineSpan_range Finite.of_fintype Submodule.eq_of_le_of_finrank_eq AffineSubspace.direction_le affineSpan_mono direction_affineSpan AffineIndependent.finrank_vectorSpan Fintype.card_fin Affine.Simplex.independent mem_affineSpan Set.mem_range_self
exists_dist_eq_circumradius_of_subset_insert_orthocenter 📖	mathematical	Set Set.instMembership Set.range Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Triangle.orthocenter Set.instHasSubset Set.instInsert	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Dist.dist PseudoMetricSpace.toDist Affine.Simplex.circumradius	—	exists_of_range_subset_orthocentricSystem instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyElemImage Set.instNonemptyElemInsert Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_image_of_finite Finite.of_fintype reflection_mem_of_le_of_mem affineSpan_mono Set.image_subset_range Affine.Simplex.circumcenter_mem_affineSpan Affine.Triangle.dist_orthocenter_reflection_circumcenter dist_reflection_eq_of_mem mem_affineSpan Set.mem_image_of_mem Set.mem_insert Affine.Simplex.dist_circumcenter_eq_circumradius Set.mem_insert_of_mem Set.mem_singleton
exists_of_range_subset_orthocentricSystem 📖	—	Set Set.instMembership Set.range Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Affine.Triangle.orthocenter Set.instHasSubset Set.instInsert	—	—	Set.mem_of_mem_insert_of_ne Set.mem_of_mem_of_subset Set.mem_range_self Set.subset_diff_singleton Set.eq_of_subset_of_card_le Set.insert_diff_self_of_notMem Set.card_range_of_injective AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent le_refl

EuclideanGeometry.OrthocentricSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineIndependent 📖	mathematical	EuclideanGeometry.OrthocentricSystem Set Set.instHasSubset Set.range	AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	—	EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter EuclideanGeometry.Cospherical.affineIndependent Set.Subset.rfl
eq_insert_orthocenter 📖	mathematical	EuclideanGeometry.OrthocentricSystem Set Set.instHasSubset Set.range Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	Set.instInsert Affine.Triangle.orthocenter	—	EuclideanGeometry.exists_of_range_subset_orthocentricSystem AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent Affine.Triangle.orthocenter_replace_orthocenter_eq_point Set.ext Set.image_univ Set.image_insert_eq Set.image_singleton Set.insert_comm Affine.Triangle.orthocenter_eq_of_range_eq
exists_circumradius_eq 📖	mathematical	EuclideanGeometry.OrthocentricSystem	Affine.Simplex.circumradius	—	EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter AffineIndependent.injective Real.instNontrivial Affine.Simplex.independent Set.subset_insert Affine.Simplex.eq_circumradius_of_dist_eq EuclideanGeometry.affineSpan_of_orthocentricSystem Set.forall_mem_range

---

← Back to Index