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