English
The range of the concatenated path γ1.trans γ2 is the union of the ranges of γ1 and γ2.
Русский
Образ пути γ1.trans γ2 равен объединению образов γ1 и γ2.
LaTeX
$$$\mathrm{range}(\gamma_1.trans \gamma_2) = \mathrm{range}(\gamma_1) \cup \mathrm{range}(\gamma_2)$$$
Lean4
theorem trans_range {a b c : X} (γ₁ : Path a b) (γ₂ : Path b c) : range (γ₁.trans γ₂) = range γ₁ ∪ range γ₂ :=
by
rw [← extend_range, ← image_univ, ← Iic_union_Ici (a := 1 / 2), image_union,
EqOn.image_eq fun t ht ↦ extend_trans_of_le_half _ _ (mem_Iic.1 ht),
EqOn.image_eq fun t ht ↦ extend_trans_of_half_le _ _ (mem_Ici.1 ht), ← image_image γ₁.extend, ←
image_image (γ₂.extend <| · - 1), ← image_image γ₂.extend]
norm_num [image_mul_left_Ici, image_mul_left_Iic, image_extend_of_subset, Icc_subset_Iic_self, Icc_subset_Ici_self]
