range_add — Mathlib

English

For natural numbers a,b, range(a+b) = range(a) ∪ (range(b)).map (addLeftEmbedding a).

Русский

Для натуральных чисел a,b выполняется range(a+b) = range(a) ∪ (range(b)).map (addLeftEmbedding a).

LaTeX

$$$\mathrm{range}(a+b) = \mathrm{range}(a) \cup (\mathrm{range}(b)).\mathrm{map}(\mathrm{addLeftEmbedding}(a))$$$

Lean4

theorem range_add (a b : ℕ) : range (a + b) = range a ∪ (range b).map (addLeftEmbedding a) :=
  by
  rw [← val_inj, union_val]
  exact Multiset.range_add_eq_union a b

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