wOppSide_vadd_right_iff — Mathlib

English

For any s, x, y, s.WOppSide x y holds if and only if there exists a point p ∈ s with Wbtw between x and p and p and y.

Русский

Для любого s, x, y выполняется: s.WOppSide x y тогда и только тогда, когда существует p ∈ s с такими свойствами, что Wbtw(x,p,y).

LaTeX

$$$$ s.WOppSide x y \iff \exists p \in s\; (Wbtw\; R\; x\; p\; y). $$$$

Lean4

theorem wOppSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y := by rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]

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