Ici_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ici_inr : Ici (inr b : α ⊕ β) = (Ici b).map Embedding.inr :=
  rfl

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