addRothNumber_Ico — Mathlib

English

For natural a,b, addRothNumber(Ico(a,b)) equals rothNumberNat(b−a).

Русский

Для натуральных a,b выполнено: addRothNumber(Ico(a,b)) = rothNumberNat(b−a).

LaTeX

$$$\\operatorname{addRothNumber}(\\mathrm{Ico}(a,b)) = \\operatorname{rothNumberNat}(b-a).$$$

Lean4

theorem addRothNumber_Ico (a b : ℕ) : addRothNumber (Ico a b) = rothNumberNat (b - a) :=
  by
  obtain h | h := le_total b a
  · rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]
  convert addRothNumber_map_add_left _ a
  rw [range_eq_Ico, map_eq_image]
  convert (image_add_left_Ico 0 (b - a) _).symm
  exact (add_tsub_cancel_of_le h).symm

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