Commit 2023-05-26 23:07 4321641d

View on Github →

feat: port Geometry.Euclidean.Basic (#4406)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Basic.lean

added theorem EuclideanGeometry.dist_affineCombination

added theorem EuclideanGeometry.dist_left_midpoint_eq_dist_right_midpoint

added theorem EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff

added theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_not_mem

added theorem EuclideanGeometry.dist_reflection

added theorem EuclideanGeometry.dist_reflection_eq_of_mem

added theorem EuclideanGeometry.dist_smul_vadd_eq_dist

added theorem EuclideanGeometry.dist_smul_vadd_sq

added theorem EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq

added theorem EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd

added theorem EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two

added theorem EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two

added theorem EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace

added theorem EuclideanGeometry.eq_reflection_of_eq_subspace

added theorem EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq

added theorem EuclideanGeometry.inner_weightedVSub

added theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjection

added theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjectionFn

added def EuclideanGeometry.orthogonalProjectionFn

added theorem EuclideanGeometry.orthogonalProjectionFn_eq

added theorem EuclideanGeometry.orthogonalProjectionFn_mem

added theorem EuclideanGeometry.orthogonalProjectionFn_mem_orthogonal

added theorem EuclideanGeometry.orthogonalProjectionFn_vsub_mem_direction_orthogonal

added theorem EuclideanGeometry.orthogonalProjection_eq_self_iff

added theorem EuclideanGeometry.orthogonalProjection_linear

added theorem EuclideanGeometry.orthogonalProjection_mem

added theorem EuclideanGeometry.orthogonalProjection_mem_orthogonal

added theorem EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self

added theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection

added theorem EuclideanGeometry.orthogonalProjection_vadd_eq_self

added theorem EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection

added theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction

added theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal

added theorem EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection

added def EuclideanGeometry.reflection

added theorem EuclideanGeometry.reflection_apply

added theorem EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq

added theorem EuclideanGeometry.reflection_eq_self_iff

added theorem EuclideanGeometry.reflection_involutive

added theorem EuclideanGeometry.reflection_mem_of_le_of_mem

added theorem EuclideanGeometry.reflection_orthogonal_vadd

added theorem EuclideanGeometry.reflection_reflection

added theorem EuclideanGeometry.reflection_symm

added theorem EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection

added theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction

added theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal