map_sub — Mathlib

English

If k ≤ n, subtract k from every element of Ico n m yields Ico (n−k) (m−k).

Русский

Если k ≤ n, вычитая k из каждого элемента Ico n m, получаем Ico (n−k) (m−k).

LaTeX

$$$\forall n,m,k:\ k \le n \Rightarrow (\operatorname{Ico}(n,m)).\operatorname{map}(x \mapsto x-k) = \operatorname{Ico}(n-k,m-k).$$$

Lean4

theorem map_sub (n m k : ℕ) (h₁ : k ≤ n) : ((Ico n m).map fun x => x - k) = Ico (n - k) (m - k) := by
  rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]

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