image_val_uIoo — Mathlib

English

Let i and j be elements of Fin(n). Then the image of the interval uIoo(i, j) under the natural embedding Fin(n) → N is the interval uIoo(i, j) in N.

Русский

Пусть i и j — элементы Fin(n). Тогда образ интервала uIoo(i, j) через естественное вложение Fin(n) → N равен интервалу uIoo(i, j) в N.

LaTeX

$$$(\uparrow) '' uIoo(i, j) = uIoo(i, j) \quad\text{for } i,j \in \mathrm{Fin}(n)$$$

Lean4

@[simp]
theorem image_val_uIoo (i j : Fin n) : (↑) '' uIoo i j = uIoo (i : ℕ) j := by simp [uIoo]

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