Lemmas about List.mapUnion operator

List.mapUnion generically (f returning any collection type)

theorem List.mapUnion₁_eq_mapUnion {β : Type u_1} {α : Type u_2} [Union β] [EmptyCollection β] (f : α → β) (as : List α) : (as.mapUnion₁ fun (x : { a : α // a ∈ as }) => f x.val) = mapUnion f as

theorem List.mapUnion₂_eq_mapUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizeOf α] [SizeOf β] [Union γ] [EmptyCollection γ] (f : α × β → γ) (xs : List (α × β)) : (xs.mapUnion₂ fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf xs }) => f x.val) = mapUnion f xs

theorem List.mapUnion₃_eq_mapUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizeOf α] [SizeOf β] [Union γ] [EmptyCollection γ] (f : α × β → γ) (xs : List (α × β)) : (xs.mapUnion₃ fun (x : { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf xs) }) => f x.val) = mapUnion f xs

@[simp]

theorem List.mapUnion_nil {β : Type u_1} {α : Type u_2} [Union β] [EmptyCollection β] (f : α → β) : mapUnion f [] = ∅

List.mapUnion for sets (f returning Set)

theorem List.mapUnion_wf {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {xs : List β} : (∀ (x : β), x ∈ xs → (f x).WellFormed) → (mapUnion f xs).WellFormed

theorem List.mapUnion_cons {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {hd : β} {tl : List β} : mapUnion f (hd :: tl) = f hd ∪ mapUnion f tl

@[simp]

theorem List.mapUnion_singleton {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {x : β} : mapUnion f [x] = f x

theorem List.mapUnion_pair {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {x y : β} : mapUnion f [x, y] = f x ∪ f y

@[simp]

theorem List.mapUnion_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {g : γ → β} {xs : List γ} : mapUnion f (map g xs) = mapUnion (f ∘ g) xs

theorem List.mem_foldl_union_iff_mem_or_exists {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {xs : List β} {init : Cedar.Data.Set α} {a : α} : a ∈ foldl (fun (as : Cedar.Data.Set α) (b : β) => as ∪ f b) init xs ↔ a ∈ init ∨ ∃ (s : β), s ∈ xs ∧ a ∈ f s

theorem List.foldl_union_wf {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {xs : List β} {init : Cedar.Data.Set α} : init.WellFormed → (∀ (x : β), x ∈ xs → (f x).WellFormed) → (foldl (fun (as : Cedar.Data.Set α) (b : β) => as ∪ f b) init xs).WellFormed

A fold of unions is well-formed if it starts from a well-formed set and adds well-formed sets.

theorem List.mem_mapUnion_iff_mem_exists {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {xs : List β} (e : α) : e ∈ mapUnion f xs ↔ ∃ (s : β), s ∈ xs ∧ e ∈ f s

theorem List.mem_mem_implies_mem_mapUnion {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {xs : List β} {e : α} {s : β} : e ∈ f s → s ∈ xs → e ∈ mapUnion f xs

theorem List.mem_implies_subset_mapUnion {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] (f : β → Cedar.Data.Set α) {xs : List β} {s : β} : s ∈ xs → f s ⊆ mapUnion f xs

@[simp]

theorem List.mapUnion_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → Cedar.Data.Set α} {g : γ → Option β} {xs : List γ} : mapUnion f (filterMap g xs) = mapUnion (fun (x : γ) => Option.mapD f Cedar.Data.Set.empty (g x)) xs

theorem List.mapUnion_congr {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] (f g : β → Cedar.Data.Set α) {xs : List β} : (∀ (b : β), b ∈ xs → f b = g b) → mapUnion f xs = mapUnion g xs

theorem List.mapUnion_eq_mapUnion_id_map {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] (f : β → Cedar.Data.Set α) {xs : List β} : mapUnion f xs = mapUnion id (map f xs)

theorem List.mapUnion_eq_of_map_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → Cedar.Data.Set α} {g : γ → Cedar.Data.Set α} {xs : List β} {ys : List γ} : map f xs = map g ys → mapUnion f xs = mapUnion g ys

theorem List.mapUnion_append {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f : β → Cedar.Data.Set α} {xs ys : List β} : mapUnion f (xs ++ ys) = mapUnion f xs ++ mapUnion f ys

theorem List.mapUnion_union_mapUnion {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (f : β → Cedar.Data.Set α) (xs ys : List β) : mapUnion f xs ∪ mapUnion f ys = mapUnion f (xs ++ ys)

Corollary of mapUnion_append, stated in reverse for some reason, and using ∪ instead of ++ (which are synonyms in the case of Data.Set)

theorem List.mapUnion_union_mapUnion' {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {f g : β → Cedar.Data.Set α} {xs : List β} : mapUnion f xs ∪ mapUnion g xs = mapUnion (fun (x : β) => f x ∪ g x) xs

mapUnion_union_mapUnion applies when you have the same function f and different input lists. mapUnion_union_mapUnion' applies when you have different functions f/g and the same input list.

theorem List.mapUnion_comm {α : Type u_1} {β : Type u_2} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → Cedar.Data.Set α} {xs ys : List β} : mapUnion f (xs ++ ys) = mapUnion f (ys ++ xs)

theorem List.map_eqv_implies_mapUnion_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → Cedar.Data.Set α} {g : γ → Cedar.Data.Set α} {xs : List β} {ys : List γ} : map f xs ≡ map g ys → mapUnion f xs = mapUnion g ys