map — Mathlib

English

Under an affine map, wOppSide is preserved: (s.map ↑f).WOppSide (f x) (f y) ↔ s.WOppSide x y.

Русский

Под образованием невырожденного отображения сохраняется wOppSide.

LaTeX

$$$$ (s.map ↑f).WOppSide (f x) (f y) \iff s.WOppSide x y. $$$$

Lean4

theorem map {s : AffineSubspace R P} {x y : P} (h : s.WOppSide x y) (f : P →ᵃ[R] P') : (s.map f).WOppSide (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

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