sOppSide_map_iff — Mathlib

English

If x and y lie strictly on opposite sides of s, then the corresponding SOppSide condition yields a nonempty set of witnesses.

Русский

Если x и y строго лежат по разные стороны s, тогда имеется ненулевое свидетельство.

LaTeX

$$$$ s.SOppSide x y \rightarrow (s).Nonempty $$$$

Lean4

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

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