image_val_Ioi

Mathlib.Order.Interval.Set.Fin

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$ \big(\operatorname{Fin.val}\big) '' \operatorname{Ioi}(i) = \operatorname{Ioo}(i, n). $$$$

Lean4

@[simp]
theorem image_val_Ioi (i : Fin n) : (↑) '' Ioi i = Ioo (i : ℕ) n := by
  rw [← preimage_val_Ioi_val, image_preimage_eq_inter_range, range_val, Ioi_inter_Iio]

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

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

Разделы

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

Аффилиация

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