range_disjoint_map_add — Mathlib

English

Let a ∈ ℕ and m be a multiset of ℕ. Then range(a) is disjoint from the multiset obtained by adding a to every element of m, i.e. Disjoint(range(a), map(t ↦ a + t) m).

Русский

Пусть a ∈ ℕ и m ∈ Multiset ℕ. Тогда диапазон a и множесто, полученное добавлением a ко всем элементам m, несовместны: Disjoint(range(a), map(t ↦ a + t) m).

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{range}(a), \\operatorname{map}(t \\mapsto a+t)\\, m)$$$

Lean4

theorem range_disjoint_map_add (a : ℕ) (m : Multiset ℕ) : Disjoint (range a) (m.map (a + ·)) :=
  by
  rw [disjoint_left]
  intro x hxa hxb
  rw [range, mem_coe, List.mem_range] at hxa
  obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
  exact (Nat.le_add_right _ _).not_gt hxa

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