English
Restricting to S1 and then mapping through the restriction to S2 is the same as mapping to S2 and restricting.
Русский
Ограничение к S1 и отображение через ограничение к S2 эквивалентно отображению к S2 и ограничению.
LaTeX
$$$ (s\restrict S_1 hS_1).map (f.restrict hfS) = s.map f hfS \restrict S_2 $$$
Lean4
/-- Restricting to `S₁` then mapping through the restriction of `f` to `S₁ →ᵃ[k] S₂` is the same
as mapping through unrestricted `f`, then restricting to `S₂`. -/
theorem restrict_map_restrict {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective f)
(S₁ : AffineSubspace k P) (S₂ : AffineSubspace k P₂) (hS₁ : affineSpan k (Set.range s.points) ≤ S₁)
(hfS : AffineSubspace.map f S₁ ≤ S₂) :
letI := Nonempty.map (AffineSubspace.inclusion hS₁) inferInstance
letI := Nonempty.map (AffineSubspace.inclusion hfS) inferInstance
(s.restrict S₁ hS₁).map (f.restrict hfS) (AffineMap.restrict.injective hf _) =
(s.map f hf).restrict S₂
(Eq.trans_le (by simp [AffineSubspace.map_span, Set.range_comp]) (AffineSubspace.map_mono f hS₁) |>.trans
hfS) :=
by rfl
