wSameSide_iff_exists_right — Mathlib

English

Let p2 ∈ s. Then s.WSameSide x y ↔ y ∈ s ∨ ∃ p1 ∈ s, SameRay(x − p1, y − p2).

Русский

Пусть p2 ∈ s. Тогда s.WSameSide x y эквивалентно y ∈ s или существует p1 ∈ s такое, что SameRay(x − p1, y − p2).

LaTeX

$$$s.WSameSide x y\iff y\in s \lor \exists p_1\in s,\ SameRay(x - p_1, y - p_2).$$$

Lean4

theorem wSameSide_iff_exists_right {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) :
    s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂) :=
  by
  rw [wSameSide_comm, wSameSide_iff_exists_left h]
  simp_rw [SameRay.sameRay_comm]

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