Iic_inl — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{Iic}(\mathrm{inl}(a)) = \mathrm{map}(\mathrm{Embedding.inl}, \mathrm{Iic}(a))$$$

Lean4

theorem Iic_inl : Iic (inl a : α ⊕ β) = (Iic a).map Embedding.inl :=
  rfl

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