sSameSide_map_iff — Mathlib

English

If h is s.SSameSide x y, then under any affine map f, h.map f provides a corresponding wSameSide relation in the image.

Русский

Если h является s.SSameSide x y, то под отображением f сохраняется связь wSameSide в образе.

LaTeX

$$$$ h.map f \text{ preserves }\text{SSameSide}. $$$$

Lean4

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

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