map_direction — Mathlib

English

The direction of the image of an affine subspace under an affine map is the image of the subspace’s direction under the linear part of the map.

Русский

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

LaTeX

$$$ (s.map f).direction = s.direction.map f.linear$$$

Lean4

@[simp]
theorem map_direction (s : AffineSubspace k P₁) : (s.map f).direction = s.direction.map f.linear := by
  simp [direction_eq_vectorSpan, AffineMap.vectorSpan_image_eq_submodule_map]

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