English
Same as map_subtype_restrict: reversing the process of mapping through a subtype and restricting returns the original simplex.
Русский
То же, что и map_subtype_restrict: разворот процесса отображения через подпроизвольное подпространство и ограничение возвращает исходный простой.
LaTeX
$$$ (s.map (AffineSubspace.subtype _) Subtype.coe_injective).restrict S (affineSpan\ le .2) = s $$$
Lean4
/-- Restricting to `affineSpan k (Set.range s.points)` can be reversed by mapping through
`AffineSubspace.subtype`. -/
@[simp]
theorem restrict_map_subtype {n : ℕ} (s : Affine.Simplex k P n) :
(s.restrict _ le_rfl).map (AffineSubspace.subtype _) Subtype.coe_injective = s :=
rfl