Iic_mk — Mathlib

English

For every index i and every a in αi, the lower set Iic inside the dependent sum at ⟨i,a⟩ coincides with the image of Iic a under the embedding σMk i: (Iic a).map (Embedding.sigmaMk i).

Русский

Для каждого индекса i и элемента a в αi множество Iic внутри зависимой суммы в точке ⟨i,a⟩ совпадает с образованием множества Iic a через вложение σMk i: (Iic a).map (Embedding.sigmaMk i).

LaTeX

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

Lean4

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

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