Lemmas on lists

Candidates for Mathlib's lemmas on lists, about the notions of core: filtering a list before List.flatMap f changes nothing when every element x with f x ≠ [] passes the filter, the counterpart of Finset.prod_filter_of_ne, next to List.flatMap_congr, and so a list without duplicates within another one without duplicates that holds every x with f x ≠ [] gives a permutation of its List.flatMap f; and a filter by a test that holds on all elements of a list or on none keeps all of it or nothing.

Main statements

• List.flatMap_filter_of_ne: a filter before List.flatMap that changes nothing.
• List.perm_flatMap_of_nodup: the List.flatMap of a list without duplicates of members of a list l without duplicates, in any order, that holds every member with a nonempty image, is a permutation of that of l.
• List.filter_eq_ite_of_forall: a filter that keeps all of a list or nothing.

theorem List.flatMap_filter_of_ne {α : Type u_1} {β : Type u_2} {l : List α} {p : α → Bool} {f : α → List β} (h : ∀ (x : α), x ∈ l → f x ≠ [] → p x = true) : flatMap f (filter p l) = flatMap f l

Filtering the list l by p before List.flatMap f changes nothing when every element x of l with f x ≠ [] satisfies p; compare Finset.prod_filter_of_ne.

theorem List.filter_eq_ite_of_forall {α : Type u_1} {l : List α} {p : α → Bool} {P : Prop} [Decidable P] (h : ∀ (a : α), a ∈ l → (p a = true ↔ P)) : filter p l = if P then l else []

Filtering by a test that holds on every element of l exactly when P holds keeps all of l or nothing.

theorem List.perm_flatMap_of_nodup {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → List β} (hl : l.Nodup) (hl' : l'.Nodup) (hsub : l' ⊆ l) (h : ∀ (x : α), x ∈ l → f x ≠ [] → x ∈ l') : (flatMap f l').Perm (flatMap f l)

A list l' without duplicates whose members lie in the list l without duplicates, and which holds every member x of l with f x ≠ [], gives a permutation of l.flatMap f, whatever the order of l': l' is a permutation of the members of l that it holds (List.perm_ext_iff_of_nodup), and the others give nothing (List.flatMap_filter_of_ne).