Ici_mk — Mathlib

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

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