restrict_map_subtype — Mathlib

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

Похожие утверждения