sOppSide_map_iff — Mathlib

English

Under an affine equivalence, SOppSide respects the image: (s.map ↑f).SOppSide (f x) (f y) ↔ s.SOppSide x y.

Русский

При аффинной эквивалентности SOppSide сохраняется в образе.

LaTeX

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

Lean4

theorem _root_.Function.Injective.sOppSide_map_iff {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'}
    (hf : Function.Injective f) : (s.map f).SOppSide (f x) (f y) ↔ s.SOppSide x y := by
  simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]

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