disjoint_reverse_right — Mathlib

English

Let l1, l2 be lists. Then l1 is disjoint from l2.reverse iff l1 is disjoint from l2.

Русский

Пусть l1, l2 — списки. Непересечение l1 и l2.reverse эквивалентно непересечению l1 и l2.

LaTeX

$$$\\operatorname{Disjoint}(L_1, \\operatorname{reverse}(L_2)) \\iff \\operatorname{Disjoint}(L_1, L_2)$$$

Lean4

@[simp]
theorem disjoint_reverse_right {l₁ l₂ : List α} : Disjoint l₁ l₂.reverse ↔ Disjoint l₁ l₂ :=
  reverse_perm _ |>.disjoint_right

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