image_cast_int_Iic

Mathlib.Data.Nat.Cast.SetInterval

URI: https://scilib.ai/kg/mathlib#Nat.image_cast_int_Iic

English

The image of the closed lower interval Iic(a) under Nat.cast is the closed lower interval Icc(0, a.cast) in ℤ.

Русский

Образ Iic(a) через Nat.cast равен Icc(0, a.cast) в ℤ.

LaTeX

$$$ \mathrm{Set.image}(\mathrm{Nat.cast}, \mathrm{Iic}(a)) = \mathrm{Icc}(0, a.cast) $$$

Lean4

theorem image_cast_int_Iic (a : ℕ) : (↑) '' Iic a = Icc (0 : ℤ) a := by rw [← Icc_bot, image_cast_int_Icc]; rfl

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

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

Разделы

Аффилиация

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