image_cast_int_Icc — Mathlib

English

The image of the closed interval Icc(a,b) under the natural-to-integer cast is the interval Icc(a,b) in ℤ.

Русский

Образ декартова интервала Icc(a,b) под отображением Nat.cast равен интервалу Icc(a.cast,b.cast) в ℤ.

LaTeX

$$$ \mathrm{Set.image}(\mathrm{Nat.cast}, \mathrm{Icc}(a,b)) = \mathrm{Icc}(a,b) \text{ (in } \mathbb{Z}) $$$

Lean4

theorem image_cast_int_Icc (a b : ℕ) : (↑) '' Icc a b = Icc (a : ℤ) b :=
  (castOrderEmbedding (α := ℤ)).image_Icc (by simp [ordConnected_Ici]) a b

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