Iic_inr — Mathlib

English

The closed right-interval from a right-injection equals the right-injection image of the corresponding right-interval: Iic(inr b) = map(Embedding.inr, Iic(b)).

Русский

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

LaTeX

$$$\mathrm{Iic}(\mathrm{inr}(b)) = \mathrm{map}(\mathrm{Embedding.inr}, \mathrm{Iic}(b))$$$

Lean4

theorem Iic_inr : Iic (inr b : α ⊕ β) = (Iic b).map Embedding.inr :=
  rfl

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