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₁ : List α} {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₁ : List α} {t₂ : List α} (p : t₁.Perm t₂) :

l.bagInter t₁ = l.bagInter t₂

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

(l₁.bagInter t₁).Perm (l₂.bagInter t₂)

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

(l ∩ (t₁ ++ t₂)).Perm (l ∩ t₁ ++ l ∩ t₂)

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

(List.take n xs).Perm (ys.inter (List.take n xs))

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

(List.drop n xs).Perm (ys.inter (List.drop n xs))

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

Documentation