Ioi_mk — Mathlib

English

For every i and a in αi, the open upper set Ioi at ⟨i,a⟩ is the image of Ioi a under σMk i: (Ioi a).map (Embedding.sigmaMk i).

Русский

Для каждого i и a ∈ αi множество Ioi в точке ⟨i,a⟩ есть образ множества Ioi a через σMk i: (Ioi a).map (Embedding.sigmaMk i).

LaTeX

$$$Ioi(\\langle i,a\\rangle)=(\\Ioi a).\\operatorname{map}(\\operatorname{Embedding.sigmaMk} i).$$$

Lean4

@[simp]
theorem Ioi_mk : Ioi (⟨i, a⟩ : Sigma α) = (Ioi a).map (Embedding.sigmaMk i) :=
  rfl

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