range_castAdd — Mathlib

English

Let m,n ∈ ℕ with m ≠ 0. The image of the embedding castAdd m : Fin n → Fin(n+m) is exactly the initial segment of Fin(n+m) consisting of elements with underlying value less than n.

Русский

Пусть m,n ∈ ℕ и m ≠ 0. Образ вкладывания castAdd m: Fin n → Fin(n+m) совпадает с начальным отрезком Fin(n+m), состоящим из элементов с базовым значением меньше n.

LaTeX

$$$$\\operatorname{range}(\\mathrm{Fin.castAdd}\\, m) = \\mathrm{Iio}(\\mathrm{Fin.natAdd}\\, n\\, 0)$$$$

Lean4

@[simp]
theorem range_castAdd [NeZero m] : range (castAdd m : Fin n → Fin (n + m)) = Iio (natAdd n 0) :=
  val_injective.image_injective <| by simp [← range_comp, comp_def]

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