Ioo_inr_inr — Mathlib

English

The open interval between two right-side injections equals the image of the open interval via Embedding.inr: Ioo(inr b1, inr b2) = map(Embedding.inr, Ioo(b1,b2)).

Русский

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

LaTeX

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

Lean4

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

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