disjoint_range_addRightEmbedding — Mathlib

English

For any a ∈ ℕ and Finset s, Disjoint (range a) (map (addRightEmbedding a) s).

Русский

Для любого a ∈ ℕ и Finset s выполняется Disjoint (range a) (map (addRightEmbedding a) s).

LaTeX

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

Lean4

theorem disjoint_range_addRightEmbedding (a : ℕ) (s : Finset ℕ) : Disjoint (range a) (map (addRightEmbedding a) s) :=
  by
  rw [← addLeftEmbedding_eq_addRightEmbedding]
  apply disjoint_range_addLeftEmbedding

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