wOppSide_map_iff — Mathlib

English

AffineMap preserves SOppSide under the map: (s.map ↑f).SOppSide (f x) (f y) ↔ s.SOppSide x y.

Русский

Аффинное отображение сохраняет SOppSide: образ имеет ту же SOppSide.

LaTeX

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

Lean4

theorem _root_.Function.Injective.wOppSide_map_iff {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'}
    (hf : Function.Injective f) : (s.map f).WOppSide (f x) (f y) ↔ s.WOppSide x y :=
  by
  refine ⟨fun h => ?_, fun h => h.map _⟩
  rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩
  rw [mem_map] at hfp₁ hfp₂
  rcases hfp₁ with ⟨p₁, hp₁, rfl⟩
  rcases hfp₂ with ⟨p₂, hp₂, rfl⟩
  refine ⟨p₁, hp₁, p₂, hp₂, ?_⟩
  simp_rw [← linearMap_vsub, (f.linear_injective_iff.2 hf).sameRay_map_iff] at h
  exact h

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