English
For every i and a in αi, the closed set Ici at ⟨i,a⟩ in the dependent sum equals the image of Ici a under σMk i: (Ici a).map (Embedding.sigmaMk i).
Русский
Для каждого i и a ∈ αi множество Ici в точке ⟨i,a⟩ равно образу Ici a через σMk i: (Ici a).map (Embedding.sigmaMk i).
LaTeX
$$$Ici(\\langle i,a\\rangle)=(\\Ici a).\\operatorname{map}(\\operatorname{Embedding.sigmaMk} i).$$$
Lean4
@[simp]
theorem Ici_mk : Ici (⟨i, a⟩ : Sigma α) = (Ici a).map (Embedding.sigmaMk i) :=
rfl