Iio_mk — Mathlib

English

For every i and a in αi, the upper-interval Iio at ⟨i,a⟩ in the dependent sum is the image of Iio a under σMk i: (Iio a).map (Embedding.sigmaMk i).

Русский

Для каждого i и a ∈ αi верхний интервал Iio в зависимой сумме равен образу Iio a через σMk i: (Iio a).map (Embedding.sigmaMk i).

LaTeX

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

Lean4

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

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