English
Restricting an affine simplex to an affine subspace S (which contains its span) yields a well-defined simplex inside S.
Русский
Ограничение аффинального простого к аффинному подпроизводному пространству S (которое содержит его афинное пространство порождающих точек) образует корректный простой внутри S.
LaTeX
$$$\text{restrict} : \text{Affine.Simplex } k P n \to \text{Affine.Simplex } k S n$$$
Lean4
/-- Restrict an affine simplex to an affine subspace that contains it. -/
@[simps]
def restrict {n : ℕ} (s : Affine.Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) :
letI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
Affine.Simplex (V := S.direction) k S n :=
letI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
{ points i := ⟨s.points i, hS <| mem_affineSpan _ <| Set.mem_range_self _⟩
independent := AffineIndependent.of_comp S.subtype s.independent }
