Commit 2025-07-08 08:06 ad70aaa7

View on Github →

feat: restricting Affine.Simplex to an affine subspace that contains it (#25172) Also removes a redundant Nonempty argument.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

modified def AffineSubspace.inclusion

added theorem AffineSubspace.map_mono

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem Affine.Simplex.map_subtype_restrict

added def Affine.Simplex.restrict

added theorem Affine.Simplex.restrict_map_inclusion

added theorem Affine.Simplex.restrict_map_restrict

added theorem Affine.Simplex.restrict_map_subtype