Ico_inr_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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