Ioc_eq_finset_map

Mathlib.Data.Int.Interval

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

English

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

Русский

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

LaTeX

$$$$\\mathrm{Ioc}(a,b) = \\{a+1, a+2, \\dots, b\\}.$$$$

Lean4

theorem Ioc_eq_finset_map :
    Ioc a b = (Finset.range (b - a).toNat).map (Nat.castEmbedding.trans <| addLeftEmbedding (a + 1)) :=
  rfl

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

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

Разделы

Аффилиация

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