English
An affine subspace s determines an opposite side relation between x and y if and only if there exists a point p in s lying on a Wbtw (weak betweenness) relation between x and y.
Русский
Для аффинного подпространства s отношение противоположной стороны между x и y существует тогда и только тогда, когда существует точка p ∈ s, лежащая в отношениях Wbtw между x и p и p и y.
LaTeX
$$$$ s.WOppSide(x,y) \iff \exists p\in s\; Wbtw(R,x,p,y). $$$$
Lean4
theorem wOppSide_iff_exists_wbtw {s : AffineSubspace R P} {x y : P} : s.WOppSide x y ↔ ∃ p ∈ s, Wbtw R x p y :=
by
refine ⟨fun h => ?_, fun ⟨p, hp, h⟩ => h.wOppSide₁₃ hp⟩
rcases h with ⟨p₁, hp₁, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
· rw [vsub_eq_zero_iff_eq] at h
rw [h]
exact ⟨p₁, hp₁, wbtw_self_left _ _ _⟩
· rw [vsub_eq_zero_iff_eq] at h
rw [← h]
exact ⟨p₂, hp₂, wbtw_self_right _ _ _⟩
· refine ⟨lineMap x y (r₂ / (r₁ + r₂)), ?_, ?_⟩
· have : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) :=
by
rw [← neg_vsub_eq_vsub_rev p₂ y]
linear_combination (norm := match_scalars <;> field_simp <;> ring) (r₁ + r₂)⁻¹ • h
rw [lineMap_apply, ← vsub_vadd x p₁, ← vsub_vadd y p₂, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, ← vadd_assoc,
vadd_eq_add, this]
exact s.smul_vsub_vadd_mem (r₂ / (r₁ + r₂)) hp₂ hp₁ hp₁
·
exact
Set.mem_image_of_mem _
⟨by positivity, div_le_one_of_le₀ (le_add_of_nonneg_left hr₁.le) (Left.add_pos hr₁ hr₂).le⟩
