English
Restricting to a smaller subspace then including into a larger one is the same as restricting directly to the larger subspace.
Русский
Ограничение к меньшему подпространству затем его включение в большее эквивалентно ограничению непосредственно до большего подпространства.
LaTeX
$$$ (s\restrict S_1 hS_1).map (\text{AffineSubspace.inclusion } hS_2) = s\restrict (S_1 \le S_2) $$
Lean4
/-- Restricting to `S₁` then mapping to a larger `S₂` is the same as restricting to `S₂`. -/
@[simp]
theorem restrict_map_inclusion {n : ℕ} (s : Affine.Simplex k P n) (S₁ S₂ : AffineSubspace k P) (hS₁) (hS₂ : S₁ ≤ S₂) :
letI := Nonempty.map (AffineSubspace.inclusion hS₁) inferInstance
letI := Nonempty.map (Set.inclusion hS₂) ‹_›
(s.restrict S₁ hS₁).map (AffineSubspace.inclusion hS₂) (Set.inclusion_injective hS₂) =
s.restrict S₂ (hS₁.trans hS₂) :=
rfl
