map_id — Mathlib

English

For every affine subspace s, applying the identity affine map leaves s unchanged.

Русский

Для любого афинного подпроизвольства s образ подAffine отображения, равный тождественному отображению, равен самому s.

LaTeX

$$$\\\\forall s:\\\\mathrm{AffineSubspace}_k P_1,\\\\ s.map(\\\\mathrm{AffineMap.id}\\\\ k P_1) = s$$$

Lean4

@[simp]
theorem map_id (s : AffineSubspace k P₁) : s.map (AffineMap.id k P₁) = s :=
  coe_injective <| image_id _

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