Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-17 20:50 0b9afe18

View on Github →

chore(linear_algebra/affine_space): redefine line_map, add to_affine_subspace (#4643)

  • now line_map takes two points on the line, not a point and a direction, update/review lemmas;
  • add submodule.to_affine_subspace;
  • add affine_map.fst and affine_map.snd;
  • prove that an affine map ℝ → ℝ sends an unordered interval to an unordered interval.

Estimated changes

added theorem set.maps_to_inter
added theorem set.maps_to_union
added theorem affine_map.coe_fst
added theorem affine_map.coe_snd
added def affine_map.fst
added theorem affine_map.fst_linear
modified def affine_map.line_map
modified theorem affine_map.line_map_apply
modified theorem affine_map.line_map_linear
deleted theorem affine_map.line_map_zero
added def affine_map.snd
added theorem affine_map.snd_linear
added theorem monotone.reflect_lt
deleted theorem reflect_lt