take_inter — Mathlib

English

For any xs, ys lists with xs ∼ ys and ys Nodup, the first n elements of xs form a permutation with the intersection of ys and xs.take n.

Русский

Пусть xs, ys — списки, xs ∼ ys, и ys Nodup. Тогда xs.take n перестановочно эквивален ys ∩ (xs.take n).

LaTeX

$$$\forall n, \; xs \sim ys \;\land\; ys.Nodup \Rightarrow (xs.take n) \sim (ys \cap (xs.take n))$$$

Lean4

theorem take_inter {xs ys : List α} (n : ℕ) (h : xs ~ ys) (h' : ys.Nodup) : xs.take n ~ ys.inter (xs.take n) :=
  by
  simp only [List.inter]
  exact
    Perm.trans
      (show xs.take n ~ xs.filter (xs.take n).elem by
        conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')])
      (Perm.filter _ h)

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