English
If you insert the endpoints x and y into the open segment between x and y, you recover the closed segment [x -[𝕜] y].
Русский
Если вставить концы x и y в открытый сегмент между x и y, получим замкнутый сегмент [x -[𝕜] y].
LaTeX
$$$\\text{insert } x (\\text{insert } y (openSegment 𝕜 x y)) = [x -[𝕜] y]$$$
Lean4
theorem insert_endpoints_openSegment (x y : E) : insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y] :=
by
simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment, openSegment_subset_segment,
true_and]
rintro z ⟨a, b, ha, hb, hab, rfl⟩
refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_
· rintro rfl
rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
· rintro rfl
rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
· exact ⟨a, b, ha', hb', hab, rfl⟩
