pairwiseDisjoint_smul_iff — Mathlib

English

Let s be a set and t a Finset. The family {x • t : x ∈ s} is pairwise disjoint if and only if the product map (p ↦ p.1 * p.2) is injective on s × t.

Русский

Пусть s — множество, t — Finset. Коллекция {x • t : x ∈ s} попарно попарно непересекается тогда и только если отображение (p) ↦ p.1 * p.2 на паре (s × t) инъективно.

LaTeX

$$$\\text{PairwiseDisjoint}(s,\\, t) \\iff (s \\times^{\\!\\!}\\! t : Set(\\alpha \\times \\alpha)).\\mathrm{InjOn}(\\lambda p. p.1 \\cdot p.2)$$$

Lean4

@[to_additive]
theorem pairwiseDisjoint_smul_iff {s : Set α} {t : Finset α} :
    s.PairwiseDisjoint (· • t) ↔ (s ×ˢ t : Set (α × α)).InjOn fun p => p.1 * p.2 := by
  simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]

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