English
A line in α-configuration and a point in a second coordinate system determine a line in the combined coordinate system.
Русский
Линия в одном пространстве и точка в другом задают линию в объединённом пространстве координат.
LaTeX
$$$ \\text{horizontal}(l,v) \\;:\\; \\text{Line } \\alpha^{(\\iota \\oplus \\iota')} , \\text{ idxFun } = \\text{Sum.elim } l.\\text{idxFun} \\; (\\text{some} \\circ v), \\text{ proper } = \\langle \\text{Sum.inl } l.\\text{proper.choose}, l.\\text{proper.choose_spec} \\rangle $$$
Lean4
/-- A line in `ι → α` and a point in `ι' → α` determine a line in `ι ⊕ ι' → α`. -/
def horizontal {α ι ι'} (l : Line α ι) (v : ι' → α) : Line α (ι ⊕ ι')
where
idxFun := Sum.elim l.idxFun (some ∘ v)
proper := ⟨Sum.inl l.proper.choose, l.proper.choose_spec⟩
