le_count_iff_replicate_le — Mathlib

English

Let a ∈ α, s a multiset, and n ∈ ℕ. Then n ≤ count a s iff replicate n a ≤ s.

Русский

Пусть a ∈ α, s — мультисет, и n ∈ ℕ. Тогда n ≤ count a s эквивалентно replicate n a ≤ s.

LaTeX

$$$$ n \\le \\operatorname{count} a s \\iff \\operatorname{replicate} n a \\le s $$$$

Lean4

theorem le_count_iff_replicate_le {a : α} {s : Multiset α} {n : ℕ} : n ≤ count a s ↔ replicate n a ≤ s :=
  Quot.inductionOn s fun _l => by
    simp only [quot_mk_to_coe'', coe_count]
    exact replicate_sublist_iff.symm.trans replicate_le_coe.symm

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