Ioc_inl_inl — Mathlib

English

The half-open interval from one left-injection to another left-injection equals the image of the corresponding half-open interval: Ioc(inl a1, inl a2) = map(Embedding.inl, Ioc(a1,a2)).

Русский

Полуоткрытый интервал между двумя левыми вложениями равен отображению соответствующего полуоткрытого интервала.

LaTeX

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

Lean4

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

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