Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-13 20:57 32c75d01

View on Github →

feat(linear_algebra/affine_space): more lemmas on directions of affine subspaces (#3377) Add more lemmas on directions of affine subspaces, motivated by uses for Euclidean geometry.

Estimated changes

Modified src/linear_algebra/affine_space.lean

added theorem affine_subspace.coe_direction_eq_vsub_set_left

added theorem affine_subspace.coe_direction_eq_vsub_set_right

added theorem affine_subspace.direction_le

added theorem affine_subspace.direction_lt_of_nonempty

added theorem affine_subspace.inter_eq_singleton_of_nonempty_of_is_compl

added theorem affine_subspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top

added theorem affine_subspace.mem_direction_iff_eq_vsub_left

added theorem affine_subspace.mem_direction_iff_eq_vsub_right

added theorem affine_subspace.sup_direction_le

added theorem affine_subspace.sup_direction_lt_of_nonempty_of_inter_empty

added theorem affine_subspace.vsub_left_mem_direction_iff_mem

added theorem affine_subspace.vsub_right_mem_direction_iff_mem