Ico_eq_finset_map

Mathlib.Data.Int.Interval

URI: https://scilib.ai/kg/mathlib#Int.Ico_eq_finset_map

English

The open-closed interval Ico(a,b) is the image of {0,...,b−a−1} under t ↦ a+t.

Русский

Пусть Ico(a,b) = {a, a+1, ..., b−1}; это образ множества {0,...,b−a−1} при отображении t ↦ a+t.

LaTeX

$$$$\\mathrm{Ico}(a,b) = \\{a, a+1, \\dots, b-1\\}.$$$$

Lean4

theorem Ico_eq_finset_map :
    Ico a b = (Finset.range (b - a).toNat).map (Nat.castEmbedding.trans <| addLeftEmbedding a) :=
  rfl

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

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

Разделы

Аффилиация

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