Ici_inl — Mathlib

English

For any a ∈ α, the upper set {inl a} is exactly the image of {a} under the left embedding, i.e., Ici(inl a) = map Embedding.inl (Ici a).

Русский

Для любого a ∈ α верхнее множество {inl a} совпадает с образом {a} через левое встроение: Ici(inl a) = map Embedding.inl (Ici a).

LaTeX

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

Lean4

theorem Ici_inl : Ici (inl a : α ⊕ β) = (Ici a).map Embedding.inl :=
  rfl

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