English
The set {y | s.SSameSide x y} equals the image2 of (t,q) ↦ t(x − p) + q with t > 0 and q ∈ s, for some p ∈ s.
Русский
Множество {y | s.SSameSide x y} совпадает с образом2 отображения (t,q) ↦ t(x − p) + q при t > 0 и q ∈ s, для некоторого p ∈ s.
LaTeX
$$$\{y \mid s.SSameSide(x,y)\} = \{ t\,(x - p) + q \;|\; t > 0,\ q \in s\},\ \text{при } x \notin s,\ p \in s.$$$
Lean4
theorem setOf_sSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
{y | s.SSameSide x y} = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) s :=
by
ext y
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ioi]
constructor
· rw [sSameSide_iff_exists_left hp]
rintro ⟨-, hy, 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
exact False.elim (hy (h.symm ▸ hp₂))
· refine ⟨r₁ / r₂, div_pos hr₁ hr₂, p₂, hp₂, ?_⟩
rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul, vsub_vadd]
· rintro ⟨t, ht, p', hp', rfl⟩
exact sSameSide_smul_vsub_vadd_right hx hp hp' ht
