wOppSide_map_iff — Mathlib

English

For any affine equivalence f, (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

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

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