sSameSide_map_iff — Mathlib

English

If f is an affine equivalence, the sSameSide relation is preserved by the map.

Русский

Если f — аффинная эквивалентность, то отношение sSameSide сохраняется под образами.

LaTeX

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

Lean4

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

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