English
A line in α-configuration and a line in another coordinate system together determine a line in the sum of coordinate systems.
Русский
Линия в одном пространстве и линия в другом задают линию в прямом суммированном пространстве координат.
LaTeX
$$$ \\text{prod}(l,l') \\;:\\; \\text{Line } \\alpha^{(\\iota \\oplus \\iota')} , \\text{ idxFun } = \\text{Sum.elim } l.\\text{idxFun} \\; l'.\\text{idxFun}, \\text{ proper } = \\langle \\text{Sum.inl } l.\\text{proper.choose}, l.\\text{proper.choose_spec} \\rangle $$$
Lean4
/-- One line in `ι → α` and one in `ι' → α` together determine a line in `ι ⊕ ι' → α`. -/
def prod {α ι ι'} (l : Line α ι) (l' : Line α ι') : Line α (ι ⊕ ι')
where
idxFun := Sum.elim l.idxFun l'.idxFun
proper := ⟨Sum.inl l.proper.choose, l.proper.choose_spec⟩
