image_val_uIcc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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