image_val_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_val_Ioo (i j : Fin n) : (↑) '' Ioo i j = Ioo (i : ℕ) j :=
  by
  rw [← preimage_val_Ioo_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans j.is_lt

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