disjoint_reverse_left — Mathlib

English

Let l1, l2 be lists. Then l1.reverse is disjoint from l2 if and only if l1 is disjoint from l2.

Русский

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

LaTeX

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

Lean4

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

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