image_val_Iio

Mathlib.Order.Interval.Set.Fin

URI: https://scilib.ai/kg/mathlib#Fin.image_val_Iio

← MathLib Explorer

English

For i ∈ Fin n, the image of Iio(i) under Fin.val equals Iio(i).

Русский

Для i ∈ Fin(n) образ Iio(i) под Fin.val равен Iio(i).

LaTeX

$$$$ \big(\operatorname{Fin.val}\big) '' \operatorname{Iio}(i) = \operatorname{Iio}(i). $$$$

Lean4

@[simp]
theorem image_val_Iio (i : Fin n) : (↑) '' Iio i = Iio (i : ℕ) :=
  by
  rw [← preimage_val_Iio_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact Iio_subset_Iio i.is_lt.le

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru