le_iff_count — Mathlib

English

The order s ≤ t holds iff for every element a, count(a, s) ≤ count(a, t).

Русский

Порядок вложения s ≤ t эквивалентен тому, что для каждого элемента a кратность a в s не больше кратности a в t.

LaTeX

$$$s \le t \iff \forall a, \operatorname{count}(a, s) \le \operatorname{count}(a, t)$$$

Lean4

theorem le_iff_count {s t : Multiset α} : s ≤ t ↔ ∀ a, count a s ≤ count a t :=
  Quotient.inductionOn₂ s t fun _ _ ↦ by simp [subperm_iff_count]

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