List Permutations and list lattice operations.

This file develops theory about the List.Perm relation and the lattice structure on lists.

theorem List.Perm.bagInter_right {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (t : List α) (h : l₁.Perm l₂) : (l₁.bagInter t).Perm (l₂.bagInter t)

theorem List.Perm.bagInter_left {α : Type u_1} [DecidableEq α] (l : List α) {t₁ t₂ : List α} (p : t₁.Perm t₂) : l.bagInter t₁ = l.bagInter t₂

theorem List.Perm.bagInter {α : Type u_1} [DecidableEq α] {l₁ l₂ t₁ t₂ : List α} (hl : l₁.Perm l₂) (ht : t₁.Perm t₂) : (l₁.bagInter t₁).Perm (l₂.bagInter t₂)

theorem List.Perm.bagInter_symm {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : (l₁.bagInter l₂).Perm (l₂.bagInter l₁)

theorem List.Perm.inter_append {α : Type u_1} [DecidableEq α] {l t₁ t₂ : List α} (h : t₁.Disjoint t₂) : (l ∩ (t₁ ++ t₂)).Perm (l ∩ t₁ ++ l ∩ t₂)

theorem List.Perm.take_inter {α : Type u_1} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : xs.Perm ys) (h' : ys.Nodup) : (List.take n xs).Perm (ys ∩ List.take n xs)

theorem List.Perm.drop_inter {α : Type u_1} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : xs.Perm ys) (h' : ys.Nodup) : (List.drop n xs).Perm (ys ∩ List.drop n xs)

theorem List.Perm.dropSlice_inter {α : Type u_1} [DecidableEq α] {xs ys : List α} (n m : ℕ) (h : xs.Perm ys) (h' : ys.Nodup) : (dropSlice n m xs).Perm (ys ∩ dropSlice n m xs)