image_val_Ici

Mathlib.Order.Interval.Set.Fin

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_val_Ici (i : Fin n) : (↑) '' Ici i = Ico (i : ℕ) n := by
  rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]

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

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

Разделы

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

Аффилиация

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