English
For an injective affine map f, (s.map f).WSameSide (f x) (f y) iff s.WSameSide x y.
Русский
Для инъективного аффинного отображения f выполняется эквивалентность: образ сохраняет wSameSide.
LaTeX
$$$$ (s.map f).WSameSide (f x) (f y) \iff s.WSameSide x y. $$$$
Lean4
theorem _root_.Function.Injective.wSameSide_map_iff {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'}
(hf : Function.Injective f) : (s.map f).WSameSide (f x) (f y) ↔ s.WSameSide 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
