Ioo_inl_inl — Mathlib

English

The open interval between two left-side injections equals the image of the corresponding open interval via Embedding.inl: Ioo(inl a1, inl a2) = map(Embedding.inl, Ioo(a1,a2)).

Русский

Открытый интервал между двумя левыми вложениями соответствует образу открытого интервала между базовыми элементами.

LaTeX

$$$\mathrm{Ioo}(\mathrm{inl}(a_1),\mathrm{inl}(a_2)) = \mathrm{map}(\mathrm{Embedding.inl}, \mathrm{Ioo}(a_1,a_2))$$$

Lean4

theorem Ioo_inl_inl : Ioo (inl a₁ : α ⊕ β) (inl a₂) = (Ioo a₁ a₂).map Embedding.inl :=
  rfl

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