English
The relation WS oppSide is symmetric in its arguments: s.WOppSide x y iff s.WOppSide y x.
Русский
Отношение WS OppSide симметрично по аргументаам: s.WOppSide x y ⇔ s.WOppSide y x.
LaTeX
$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P,\; s.WOppSide\; x\; y \iff s.WOppSide\; y\; x$$$
Lean4
theorem wSameSide_vadd_left_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y := by
constructor
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
refine ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩
rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
refine ⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, p₂, hp₂, ?_⟩
rwa [vadd_vsub_vadd_cancel_left]
