disjoint_range_addLeftEmbedding — Mathlib

English

For any a ∈ ℕ and any Finset s, the sets range a and map (addLeftEmbedding a) s are disjoint.

Русский

Для любого a ∈ ℕ и конечного множества s множества range a и map (addLeftEmbedding a) s попарно непересекаются.

LaTeX

$$$\forall a\in\mathbb{N},\forall s\in\mathrm{Finset}\,\mathbb{N},\ \mathrm{Disjoint}(\mathrm{range}(a), \mathrm{map}(\mathrm{addLeftEmbedding}(a), s))$$$

Lean4

theorem disjoint_range_addLeftEmbedding (a : ℕ) (s : Finset ℕ) : Disjoint (range a) (map (addLeftEmbedding a) s) :=
  by
  simp_rw [disjoint_left, mem_map, mem_range, addLeftEmbedding_apply]
  rintro _ h ⟨l, -, rfl⟩
  cutsat

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