Ico_inl_inl — Mathlib

English

The half-open interval between two left-side injections corresponds to the image of the half-open interval on the base elements under Embedding.inl: Ico(inl a1, inl a2) = map(Embedding.inl, Ico(a1,a2)).

Русский

Полуоткрытый интервал между двумя левыми инъекциями превращается в образ полуоткрытого интервала между базовыми элементами через Embedding.inl.

LaTeX

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

Lean4

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

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