image_cast_int_Ico — Mathlib

English

The image of the half-open interval Ico(a,b) under Nat.cast is the half-open interval Ico(a.cast,b.cast) in ℤ.

Русский

Образ полуоткрытого интервала Ico(a,b) через Nat.cast даёт интервал Ico(a.cast,b.cast) в ℤ.

LaTeX

$$$ \mathrm{Set.image}(\mathrm{Nat.cast}, \mathrm{Ico}(a,b)) = \mathrm{Ico}(a.cast,b.cast) $$$

Lean4

theorem image_cast_int_Ico (a b : ℕ) : (↑) '' Ico a b = Ico (a : ℤ) b :=
  (castOrderEmbedding (α := ℤ)).image_Ico (by simp [ordConnected_Ici]) a b

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