disjoint_toFinset_iff_disjoint — Mathlib

English

For lists l, l', the disjointness of their toFinset representations is equivalent to the lists being disjoint.

Русский

Для списков l, l' непересечение их представлений через toFinset эквивалентно тому, что сами списки не имеют общих элементов.

LaTeX

$$$\\operatorname{Disjoint}(l^{toFinset}, l'^{toFinset}) \\iff l.Disjoint l'$$$

Lean4

@[simp]
theorem disjoint_toFinset_iff_disjoint : _root_.Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l' :=
  Multiset.disjoint_toFinset.trans (Multiset.coe_disjoint _ _)

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