Ioi_inr — Mathlib

English

For any b ∈ β, the open upper set {inr b} equals the image of {b} under the right embedding, i.e., Ioi(inr b) = map Embedding.inr (Ioi b).

Русский

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

LaTeX

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

Lean4

theorem Ioi_inr : Ioi (inr b : α ⊕ β) = (Ioi b).map Embedding.inr :=
  rfl

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