range_add_eq_union — Mathlib

English

Let a,b ∈ ℕ. Then range(a+b) = range(a) ∪ map(t ↦ a+t) range(b).

Русский

Пусть a,b ∈ ℕ. Тогда range(a+b) = range(a) ∪ map(t ↦ a+t) range(b).

LaTeX

$$$\\operatorname{range}(a+b) = \\operatorname{range}(a) \\cup \\operatorname{map}(t \\mapsto a+t)\\operatorname{range}(b)$$$

Lean4

theorem range_add_eq_union (a b : ℕ) : range (a + b) = range a ∪ (range b).map (a + ·) :=
  by
  rw [range_add, add_eq_union_iff_disjoint]
  apply range_disjoint_map_add

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