image_val_uIoc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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