Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-06 20:20 f548db40

View on Github →

feat(linear_algebra/affine_space): lattice structure on affine subspaces (#3288) Define a complete_lattice instance on affine subspaces of an affine space, and prove a few basic lemmas relating to it. (There are plenty more things that could be proved about it, that I think can reasonably be added later.)

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem add_torsor.vsub_set_empty

Modified src/linear_algebra/affine_space.lean

added theorem affine_space.vector_span_def

added theorem affine_subspace.affine_span_eq_Inf

added theorem affine_subspace.bot_coe

added theorem affine_subspace.direction_bot

added theorem affine_subspace.direction_inf

added theorem affine_subspace.direction_top

added theorem affine_subspace.exists_of_lt

added theorem affine_subspace.inf_coe

added theorem affine_subspace.le_def'

added theorem affine_subspace.le_def

added theorem affine_subspace.lt_def

added theorem affine_subspace.lt_iff_le_and_exists

added theorem affine_subspace.mem_inf_iff

added theorem affine_subspace.mem_top

deleted theorem affine_subspace.mem_univ

added theorem affine_subspace.not_le_iff_exists

added theorem affine_subspace.not_mem_bot

added theorem affine_subspace.span_Union

added theorem affine_subspace.span_empty

added theorem affine_subspace.span_points_subset_coe_of_subset_coe

added theorem affine_subspace.span_union

added theorem affine_subspace.span_univ

added theorem affine_subspace.top_coe

deleted def affine_subspace.univ

deleted theorem affine_subspace.univ_coe