map — Mathlib

English

If s.WSameSide x y, then for any affine map f, (s.map f).WSameSide (f x) (f y).

Русский

Если x и y лежат на одной стороне по s, то их изображение под отображением f тоже сохраняет это свойство.

LaTeX

$$$$ s.WSameSide x y \rightarrow (s.map f).WSameSide (f x) (f y). $$$$

Lean4

theorem map {s : AffineSubspace R P} {x y : P} (h : s.WSameSide x y) (f : P →ᵃ[R] P') :
    (s.map f).WSameSide (f x) (f y) := by
  rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩
  refine ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩
  simp_rw [← linearMap_vsub]
  exact h.map f.linear

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