rel_associated_iff_map_eq_map — Mathlib

English

Two multisets p and q are related by Associated if and only if their images under the map mk are equal.

Русский

Две мультисеты связаны отношением Associated тогда и только тогда, когда их образы под отображением mk совпадают.

LaTeX

$$Multiset.Rel Associated p q ↔ p.map Associates.mk = q.map Associates.mk$$

Lean4

theorem rel_associated_iff_map_eq_map {p q : Multiset M} :
    Multiset.Rel Associated p q ↔ p.map Associates.mk = q.map Associates.mk :=
  by
  rw [← Multiset.rel_eq, Multiset.rel_map]
  simp only [mk_eq_mk_iff_associated]

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