English
Let x and y be elements of the product space ⋯ over i. Then every point on the segment between x and y has its i-th coordinate lying in the segment between x_i and y_i for every i.
Русский
Пусть x и y принадлежат произведению пространств ⋯. Тогда любая точка z на отрезке между x и y имеет i-ю координату z_i, принадлежащую отрезку между x_i и y_i для каждого i.
LaTeX
$$$$\operatorname{segment}_{\mathbb{k}}(x,y) \subseteq s\,\pi\,\lambda i.\operatorname{segment}_{\mathbb{k}}(x_i,y_i).$$$$
Lean4
theorem segment_subset (x y : ∀ i, M i) : segment 𝕜 x y ⊆ s.pi fun i => segment 𝕜 (x i) (y i) :=
by
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩
