English
The set {y | s.WOppSide x y} equals the image2 of (t,q) ↦ t(x − p) + q with t ≤ 0 and q ∈ s, for some p ∈ s.
Русский
Множество {y | s.WOppSide x y} совпадает с образом2 отображения (t,q) ↦ t(x − p) + q при t ≤ 0 и q ∈ s, для некоторого p ∈ s.
LaTeX
$$$\{y \mid s.WOppSide(x,y)\} = \{ t\,(x - p) + q \;|\; t \le 0,\ q \in s\},\ \text{при } x \notin s,\ p \in s.$$$
Lean4
theorem setOf_wOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
{y | s.WOppSide x y} = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) s :=
by
ext y
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iic]
constructor
· rw [wOppSide_iff_exists_left hp, or_iff_right hx]
rintro ⟨p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
· rw [vsub_eq_zero_iff_eq] at h
exact False.elim (hx (h.symm ▸ hp))
· rw [vsub_eq_zero_iff_eq] at h
refine ⟨0, le_rfl, p₂, hp₂, ?_⟩
simp [h]
· refine ⟨-r₁ / r₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂).le, p₂, hp₂, ?_⟩
rw [div_eq_inv_mul, ← smul_smul, neg_smul, h, smul_neg, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
neg_vsub_eq_vsub_rev, vsub_vadd]
· rintro ⟨t, ht, p', hp', rfl⟩
exact wOppSide_smul_vsub_vadd_right x hp hp' ht
