English
The set of points on the same side as x with respect to s is the image2 of the map (t,q) ↦ t(x − p) + q with t ≥ 0 and q ∈ s, for some p ∈ s.
Русский
Множество y, лежащих по той же стороне относительно s, есть образ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 \ge 0,\ q \in s\},\ \text{при } x \notin s,\ p \in s.$$$
Lean4
theorem setOf_wSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
{y | s.WSameSide x y} = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) s :=
by
ext y
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ici]
constructor
· rw [wSameSide_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_pos hr₁ hr₂).le, 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 wSameSide_smul_vsub_vadd_right x hp hp' ht
