toEnumFinset_subset_iff — Mathlib

English

m1.toEnumFinset ⊆ m2.toEnumFinset if and only if m1 ≤ m2.

Русский

m1.toEnumFinset ⊆ m2.toEnumFinset тогда и только тогда, когда m1 ≤ m2.

LaTeX

$$m₁.toEnumFinset ⊆ m₂.toEnumFinset \iff m₁ ≤ m₂$$

Lean4

@[simp]
theorem toEnumFinset_subset_iff {m₁ m₂ : Multiset α} : m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂ :=
  ⟨fun h ↦ by simpa using map_fst_le_of_subset_toEnumFinset h, Multiset.toEnumFinset_mono⟩

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