English
For any x,y ∈ P, the R'-affine segment is contained in the R-affine segment: affineSegment(R', x, y) ⊆ affineSegment(R, x, y).
Русский
Для любых x,y ∈ P аффинный отрезок над R' содержится в аффинном отрезке над R: affineSegment(R', x, y) ⊆ affineSegment(R, x, y).
LaTeX
$$$\text{affineSegment}(R', x, y) \subseteq \text{affineSegment}(R, x, y)$$$
Lean4
theorem lift (x y : P) : affineSegment R' x y ⊆ affineSegment R x y :=
by
rintro p ⟨a, ⟨⟨ha₀, ha₁⟩, rfl⟩⟩
refine ⟨a • 1, ⟨?_, ?_⟩, by simp [lineMap_apply]⟩
· rw [← zero_smul R' (1 : R)]
exact smul_le_smul_of_nonneg_right ha₀ zero_le_one
· nth_rw 2 [← one_smul R' 1]
exact smul_le_smul_of_nonneg_right ha₁ zero_le_one
