Ioc_inr_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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