Commit 2020-08-04 10:47 8f02ad2f

View on Github →

feat(geometry/euclidean): orthogonal projection (#3662) Define orthogonal projection onto an affine subspace of a Euclidean affine space, and prove some basic lemmas about it.

Estimated changes

Modified src/geometry/euclidean.lean

added theorem euclidean_geometry.dist_orthogonal_projection_eq_zero_iff

added theorem euclidean_geometry.dist_orthogonal_projection_ne_zero_of_not_mem

added theorem euclidean_geometry.dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square

added theorem euclidean_geometry.dist_square_smul_orthogonal_vadd_smul_orthogonal_vadd

added theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection

added theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection_fn

added def euclidean_geometry.orthogonal_projection

added theorem euclidean_geometry.orthogonal_projection_eq_self_iff

added def euclidean_geometry.orthogonal_projection_fn

added theorem euclidean_geometry.orthogonal_projection_fn_eq

added theorem euclidean_geometry.orthogonal_projection_fn_mem

added theorem euclidean_geometry.orthogonal_projection_fn_mem_orthogonal

added theorem euclidean_geometry.orthogonal_projection_fn_vsub_mem_direction_orthogonal

added theorem euclidean_geometry.orthogonal_projection_mem

added theorem euclidean_geometry.orthogonal_projection_mem_orthogonal

added theorem euclidean_geometry.orthogonal_projection_vadd_eq_self

added theorem euclidean_geometry.orthogonal_projection_vadd_smul_vsub_orthogonal_projection

added theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction

added theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction_orthogonal

added theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction

added theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction_orthogonal