wSameSide_map_iff — Mathlib

English

Under an affine equivalence, wSameSide is preserved: (s.map ↑f).WSameSide (f x) (f y) ↔ s.WSameSide x y.

Русский

При аффинном эквиваленте сохраняется свойство wSameSide.

LaTeX

$$$$ (s.map \uparrow f).WSameSide (f x) (f y) \iff s.WSameSide x y. $$$$

Lean4

@[simp]
theorem _root_.AffineEquiv.wSameSide_map_iff {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P') :
    (s.map ↑f).WSameSide (f x) (f y) ↔ s.WSameSide x y :=
  (show Function.Injective f.toAffineMap from f.injective).wSameSide_map_iff

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