English
For any list l of natural numbers, the family of lists produced by ranges(l) are pairwise disjoint
Русский
Для любого списка натуральных чисел пары списков, полученные через ranges(l), попарочно не пересекаются.
LaTeX
$$$\mathrm{Pairwise}\;\mathrm{Disjoint}(\mathrm{ranges}(l))$$$
Lean4
/-- The members of `l.ranges` are pairwise disjoint -/
theorem ranges_disjoint (l : List ℕ) : Pairwise Disjoint (ranges l) := by
induction l with
| nil => exact Pairwise.nil
| cons a l hl =>
simp only [ranges, pairwise_cons]
constructor
· intro s hs
obtain ⟨s', _, rfl⟩ := mem_map.mp hs
intro u hu
rw [mem_map]
rw [mem_range] at hu
cutsat
· rw [pairwise_map]
apply Pairwise.imp _ hl
intro u v
apply disjoint_map
exact fun u v => Nat.add_left_cancel
