sSameSide_iff_exists_right — Mathlib

English

Let h encode Wbtw x y z with z ∈ s; then s.WSameSide x y iff x ∈ s or there exists p2 ∈ s with SameRay.

Русский

Пусть h кодирует Wbtw x y z, и z ∈ s; тогда s.WSameSide x y эквивалентно x ∈ s или существует p2 ∈ s с SameRay.

LaTeX

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

Lean4

theorem sSameSide_iff_exists_right {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) :
    s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂) :=
  by
  rw [sSameSide_comm, sSameSide_iff_exists_left h, ← and_assoc, and_comm (a := y ∉ s), and_assoc]
  simp_rw [SameRay.sameRay_comm]

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