WOppSide — Mathlib

English

Under an injective affine map f, the weak opposite side relation is preserved by the image: (s.map f).WOppSide (f x) (f y) iff s.WOppSide x y.

Русский

При инъективном аффинном отображении f слабая противоположная сторона сохраняется в образе: (s.map f).WOppSide (f x) (f y) эквивалентно s.WOppSide x y.

LaTeX

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

Lean4

/-- The points `x` and `y` are weakly on opposite sides of `s`. -/
def WOppSide (s : AffineSubspace R P) (x y : P) : Prop :=
  ∃ᵉ (p₁ ∈ s) (p₂ ∈ s), SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

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