English
The closed left-interval from a left-injection equals the left-injection image of the corresponding left-interval: Iic(inl a) = map(Embedding.inl, Iic(a)).
Русский
Замкнутый левый интервал от вложения inl эквивалентен отображению левого интервала через Embedding.inl.
LaTeX
$$$\mathrm{Iic}(\mathrm{inl}(a)) = \mathrm{map}(\mathrm{Embedding.inl}, \mathrm{Iic}(a))$$$
Lean4
theorem Iic_inl : Iic (inl a : α ⊕ β) = (Iic a).map Embedding.inl :=
rfl