le_replicate_iff — Mathlib

English

For m ∈ Multiset α, m ≤ replicate n a iff ∃ k ≤ n, m = replicate k a.

Русский

Для множества m ∈ Multiset α: m ≤ replicate n a тогда и только тогда, когда существует k ≤ n, такое что m = replicate k a.

LaTeX

$$$ m \\le \\operatorname{replicate}(n,a) \\iff \\exists k \\le n, \\operatorname{replicate}(k,a) = m$$$

Lean4

theorem le_replicate_iff {m : Multiset α} {a : α} {n : ℕ} : m ≤ replicate n a ↔ ∃ k ≤ n, m = replicate k a :=
  ⟨fun h =>
    ⟨card m, (card_mono h).trans_eq (card_replicate _ _),
      eq_replicate_card.2 fun _ hb => eq_of_mem_replicate <| subset_of_le h hb⟩,
    fun ⟨_, hkn, hm⟩ => hm.symm ▸ (replicate_le_replicate _).2 hkn⟩

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