range_add_eq_union — Mathlib

English

The range of a+b is the union of the range of a and the map of the range of b under addition by a.

Русский

Диапазон a+b является объединением диапазона a и образа диапазона b под сложением на a.

LaTeX

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

Lean4

theorem range_add_eq_union : range (a + b) = range a ∪ (range b).map (addLeftEmbedding a) :=
  by
  rw [Finset.range_eq_Ico, map_eq_image]
  convert (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm
  ext x
  simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]
  constructor
  · cutsat
  · rintro h
    exact ⟨x - a, by cutsat⟩

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