coe_eq_coe — Mathlib

English

Equality of two coerced lists to multisets is equivalent to permutation.

Русский

Равенство двух образующих списков как мультимножества эквивалентно тому, что списки являются перестановкой.

LaTeX

$$$$(l_1 : Multiset\ α) = (l_2 : Multiset\ α) \iff l_1 \Sim l_2 $$$$

Lean4

@[simp]
theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Multiset α) = l₂ ↔ l₁ ~ l₂ :=
  Quotient.eq

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