Icc_inr_inr — Mathlib

English

The closed interval between two right-side injections equals the right injection image of the interval: Icc(inr b1, inr b2) = map(Embedding.inr, Icc(b1,b2)).

Русский

Замкнутый интервал между двумя правыми вложениями равен изображению интервала правым вложением.

LaTeX

$$$\mathrm{Icc}(\mathrm{inr}(b_1),\mathrm{inr}(b_2)) = \mathrm{map}(\mathrm{Embedding.inr}, \mathrm{Icc}(b_1,b_2))$$$

Lean4

theorem Icc_inr_inr : Icc (inr b₁ : α ⊕ β) (inr b₂) = (Icc b₁ b₂).map Embedding.inr :=
  rfl

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