SOppSide — Mathlib

English

Similarly, the strict opposite side relation is preserved by injective affine maps: (s.map f).SOppSide (f x) (f y) iff s.SOppSide x y.

Русский

Аналогично: строгое противоположное положение сохраняется под образами инъективных аффинных отображений.

LaTeX

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

Lean4

/-- The points `x` and `y` are strictly on opposite sides of `s`. -/
def SOppSide (s : AffineSubspace R P) (x y : P) : Prop :=
  s.WOppSide x y ∧ x ∉ s ∧ y ∉ s

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