English
If z lies on the line through x and y (i.e., z ∈ range(lineMap x y)), then the open segment between x and y is contained in the union of the open segment from x to z, the open segment from z to y, and the point z.
Русский
Если z лежит на прямой через x и y (то есть z ∈ range(lineMap x y)), то открытый сегмент между x и y содержится в объединении открытого сегмента xz, yz и точки z.
LaTeX
$$$ z \in range( lineMap_{\mathbb{k}}(x,y) ) \implies openSegment_{\mathbb{k}}(x,y) \subseteq \{z\} \cup openSegment_{\mathbb{k}}(x,z) \cup openSegment_{\mathbb{k}}(z,y) $$$
Lean4
/-- If `z = lineMap x y c` is a point on the line passing through `x` and `y`, then the open
segment `openSegment 𝕜 x y` is included in the union of the open segments `openSegment 𝕜 x z`,
`openSegment 𝕜 z y`, and the point `z`. Informally, `(x, y) ⊆ {z} ∪ (x, z) ∪ (z, y)`. -/
theorem openSegment_subset_union (x y : E) {z : E} (hz : z ∈ range (lineMap x y : 𝕜 → E)) :
openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y) :=
by
rcases hz with ⟨c, rfl⟩
simp only [openSegment_eq_image_lineMap, ← mapsTo_iff_image_subset]
rintro a ⟨h₀, h₁⟩
rcases lt_trichotomy a c with (hac | rfl | hca)
· right
left
have hc : 0 < c := h₀.trans hac
refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']
· left
rfl
· right
right
have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
simp only [← lineMap_apply_one_sub y]
refine ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩, ?_⟩
simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul, div_mul_cancel₀ _ hc.ne',
sub_sub_sub_cancel_right]
