Ioi_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioi_inl : Ioi (inl a : α ⊕ β) = (Ioi a).map Embedding.inl :=
  rfl

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