le_nsmul_iff_le — Mathlib

English

For s,t multisets, if s is nodup and n ≠ 0, then s ≤ n • t iff s ≤ t.

Русский

Для s,t мультимножествах, если s без повторов, и n ≠ 0, то s ≤ n • t тогда и только тогда s ≤ t.

LaTeX

$$$s\;\text{Nodup} \Rightarrow (n \neq 0) \Rightarrow (s \le n \cdot t \iff s \le t).$$$

Lean4

theorem le_nsmul_iff_le {s t : Multiset α} {n : ℕ} (h : s.Nodup) (hn : n ≠ 0) : s ≤ n • t ↔ s ≤ t := by
  classical simp [← h.le_dedup_iff_le, hn]

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