Icc_inl_inl — Mathlib

English

The closed interval between two left-side injections equals the left injection of the interval between the corresponding base elements: Icc(inl a1, inl a2) = map(Embedding.inl, Icc(a1,a2)).

Русский

Замкнутый интервал между двумя левыми инъекциями равен отображению интервала между базовыми элементами через вложение inl.

LaTeX

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

Lean4

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

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