inter_reverse — Mathlib

English

The intersection with a list and the reverse of another list are invariant under reversing the second argument: xs ∩ ys.reverse = xs ∩ ys.

Русский

Пересечение xs и обратного списка ys не изменяется при развороте второго аргумента: xs ∩ ys.reverse = xs ∩ ys.

LaTeX

$$$\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {xs ys : List \\\\alpha}, xs.\\\\inter ys.reverse = xs.\\\\inter ys$$$

Lean4

@[simp]
theorem inter_reverse {xs ys : List α} : xs.inter ys.reverse = xs.inter ys := by
  simp only [List.inter, elem_eq_mem, mem_reverse]

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