English
Under the same hypotheses as above, the closed interval between a and b in WithBot α is obtained by embedding the closed interval [a, b] in α into WithBot α via the natural embedding x ↦ some x. In particular, Icc(a:WithBot α) b = (Icc a b).map Embedding.some.
Русский
При тех же условиях конвертации, замкнутый интервал между a и b в WithBot α получается путем отображения замкнутого интервала [a, b] из α в WithBot α через естественное вложение x ↦ Some x. Иными словами, Icc(a:WithBot α) b = (Icc a b).map Embedding.some.
LaTeX
$$$$ \\mathrm{Icc}(a : \\mathrm{WithBot}\\ α) \\\\ b = \\bigl( \\mathrm{Icc} \\, a \\, b \\bigr).\\mathrm{map}\\, \\mathrm{Embedding}.some. $$$$
Lean4
theorem Icc_coe_coe : Icc (a : WithBot α) b = (Icc a b).map Embedding.some :=
rfl
