Iio_inl — Mathlib

English

The open left-interval from a left-injection equals the left-injection image of the open interval: Iio(inl a) = map(Embedding.inl, Iio(a)).

Русский

Открытый левый интервал от вложения inl равен отображению открытого интервала через Embedding.inl.

LaTeX

$$$\mathrm{Iio}(\mathrm{inl}(a)) = \mathrm{map}(\mathrm{Embedding.inl}, \mathrm{Iio}(a))$$$

Lean4

theorem Iio_inl : Iio (inl a : α ⊕ β) = (Iio a).map Embedding.inl :=
  rfl

Похожие утверждения