Commit 2023-06-28 18:22 ec733a5a

View on Github →

feat: port Geometry.Euclidean.MongePoint (#5056)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/MongePoint.lean

added theorem Affine.Simplex.affineSpan_pair_eq_altitude_iff

added def Affine.Simplex.altitude

added theorem Affine.Simplex.altitude_def

added theorem Affine.Simplex.direction_altitude

added theorem Affine.Simplex.direction_mongePlane

added theorem Affine.Simplex.eq_mongePoint_of_forall_mem_mongePlane

added theorem Affine.Simplex.finrank_direction_altitude

added theorem Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub

added theorem Affine.Simplex.mem_altitude

added def Affine.Simplex.mongePlane

added theorem Affine.Simplex.mongePlane_comm

added theorem Affine.Simplex.mongePlane_def

added def Affine.Simplex.mongePoint

added def Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter

added theorem Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub

added def Affine.Simplex.mongePointWeightsWithCircumcenter

added theorem Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter

added theorem Affine.Simplex.mongePoint_eq_of_range_eq

added theorem Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter

added theorem Affine.Simplex.mongePoint_mem_affineSpan

added theorem Affine.Simplex.mongePoint_mem_mongePlane

added theorem Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter

added theorem Affine.Simplex.sum_mongePointVSubFaceCentroidWeightsWithCircumcenter

added theorem Affine.Simplex.sum_mongePointWeightsWithCircumcenter

added theorem Affine.Simplex.vectorSpan_isOrtho_altitude_direction

added theorem Affine.Triangle.affineSpan_orthocenter_point_le_altitude

added theorem Affine.Triangle.altitude_eq_mongePlane

added theorem Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan

added theorem Affine.Triangle.dist_orthocenter_reflection_circumcenter

added theorem Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset

added theorem Affine.Triangle.eq_orthocenter_of_forall_mem_altitude

added def Affine.Triangle.orthocenter

added theorem Affine.Triangle.orthocenter_eq_mongePoint

added theorem Affine.Triangle.orthocenter_eq_of_range_eq

added theorem Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter

added theorem Affine.Triangle.orthocenter_mem_affineSpan

added theorem Affine.Triangle.orthocenter_mem_altitude

added theorem Affine.Triangle.orthocenter_replace_orthocenter_eq_point

added theorem EuclideanGeometry.OrthocentricSystem.affineIndependent

added theorem EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter

added theorem EuclideanGeometry.OrthocentricSystem.exists_circumradius_eq

added def EuclideanGeometry.OrthocentricSystem

added theorem EuclideanGeometry.affineSpan_of_orthocentricSystem

added theorem EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter

added theorem EuclideanGeometry.exists_of_range_subset_orthocentricSystem