toEnumFinset_mono — Mathlib

English

If m1 ≤ m2 as multisets, then m1.toEnumFinset ⊆ m2.toEnumFinset.

Русский

Если m1 ≤ m2 как мультимножества, то m1.toEnumFinset ⊆ m2.toEnumFinset.

LaTeX

$$m₁ \le m₂ \,→\, m₁.toEnumFinset ⊆ m₂.toEnumFinset$$

Lean4

@[mono]
theorem toEnumFinset_mono {m₁ m₂ : Multiset α} (h : m₁ ≤ m₂) : m₁.toEnumFinset ⊆ m₂.toEnumFinset :=
  by
  intro p
  simp only [Multiset.mem_toEnumFinset]
  exact lt_of_le_of_lt' (Multiset.le_iff_count.mp h p.1)

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