map_valEmbedding_Ioi

Mathlib.Order.Interval.Finset.Fin

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

English

The Nat-valued image of Ioi(a) equals Ioo(a.val,n).

Русский

Изображение Ioi(a) через valEmbedding даёт Ioo(a.val,n).

LaTeX

$$$(\operatorname{Finset.Ioi}\ a).\mathrm{map}\ \mathrm{valEmbedding} = \operatorname{Finset.Ioo}(a.\mathrm{val}, n)$$$

Lean4

@[simp]
theorem map_valEmbedding_Ioi : (Ioi a).map Fin.valEmbedding = Ioo (a : ℕ) n := by
  rw [← attachFin_Ioo_eq_Ioi, map_valEmbedding_attachFin]

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

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

Разделы

Аффилиация

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