Documentation

Mathlib.Data.List.Sigma

Utilities for lists of sigmas #

This file includes several ways of interacting with List (Sigma β), treated as a key-value store.

If α : Type* and β : α → Type*, then we regard s : Sigma β as having key s.1 : α and value s.2 : β s.1. Hence, List (Sigma β) behaves like a key-value store.

Main Definitions #

keys #

def List.keys {α : Type u} {β : αType v} :
List (Sigma β)List α

List of keys from a list of key-value pairs

Equations
@[simp]
theorem List.keys_nil {α : Type u} {β : αType v} :
@[simp]
theorem List.keys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
(s :: l).keys = s.fst :: l.keys
theorem List.mem_keys_of_mem {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
s ls.fst l.keys
theorem List.exists_of_mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} (h : a l.keys) :
(b : β a), a, b l
theorem List.mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
a l.keys (b : β a), a, b l
theorem List.notMem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
¬a l.keys ∀ (b : β a), ¬a, b l
@[deprecated List.notMem_keys (since := "2025-05-23")]
theorem List.not_mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
¬a l.keys ∀ (b : β a), ¬a, b l

Alias of List.notMem_keys.

theorem List.ne_key {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
¬a l.keys ∀ (s : Sigma β), s la s.fst
@[deprecated List.ne_key (since := "2025-04-27")]
theorem List.not_eq_key {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
¬a l.keys ∀ (s : Sigma β), s la s.fst

Alias of List.ne_key.

NodupKeys #

def List.NodupKeys {α : Type u} {β : αType v} (l : List (Sigma β)) :

Determines whether the store uses a key several times.

Equations
theorem List.nodupKeys_iff_pairwise {α : Type u} {β : αType v} {l : List (Sigma β)} :
l.NodupKeys Pairwise (fun (s s' : Sigma β) => s.fst s'.fst) l
theorem List.NodupKeys.pairwise_ne {α : Type u} {β : αType v} {l : List (Sigma β)} (h : l.NodupKeys) :
Pairwise (fun (s s' : Sigma β) => s.fst s'.fst) l
@[simp]
theorem List.nodupKeys_nil {α : Type u} {β : αType v} :
@[simp]
theorem List.nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
theorem List.notMem_keys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) :
@[deprecated List.notMem_keys_of_nodupKeys_cons (since := "2025-05-23")]
theorem List.not_mem_keys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) :

Alias of List.notMem_keys_of_nodupKeys_cons.

theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) :
theorem List.NodupKeys.eq_of_fst_eq {α : Type u} {β : αType v} {l : List (Sigma β)} (nd : l.NodupKeys) {s s' : Sigma β} (h : s l) (h' : s' l) :
s.fst = s'.fsts = s'
theorem List.NodupKeys.eq_of_mk_mem {α : Type u} {β : αType v} {a : α} {b b' : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : a, b l) (h' : a, b' l) :
b = b'
theorem List.nodupKeys_singleton {α : Type u} {β : αType v} (s : Sigma β) :
theorem List.NodupKeys.sublist {α : Type u} {β : αType v} {l₁ l₂ : List (Sigma β)} (h : l₁.Sublist l₂) :
l₂.NodupKeysl₁.NodupKeys
theorem List.NodupKeys.nodup {α : Type u} {β : αType v} {l : List (Sigma β)} :
theorem List.perm_nodupKeys {α : Type u} {β : αType v} {l₁ l₂ : List (Sigma β)} (h : l₁.Perm l₂) :
theorem List.nodupKeys_flatten {α : Type u} {β : αType v} {L : List (List (Sigma β))} :
L.flatten.NodupKeys (∀ (l : List (Sigma β)), l Ll.NodupKeys) Pairwise Disjoint (map keys L)
@[deprecated List.nodup_zipIdx_map_snd (since := "2025-01-28")]
theorem List.nodup_enum_map_fst {α : Type u} (l : List α) :

Alias of List.nodup_zipIdx_map_snd.

theorem List.mem_ext {α : Type u} {β : αType v} {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.Nodup) (nd₁ : l₁.Nodup) (h : ∀ (x : Sigma β), x l₀ x l₁) :
l₀.Perm l₁

dlookup #

def List.dlookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
List (Sigma β)Option (β a)

dlookup a l is the first value in l corresponding to the key a, or none if no such element exists.

Equations
@[simp]
theorem List.dlookup_nil {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
@[simp]
theorem List.dlookup_cons_eq {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) :
dlookup a (a, b :: l) = some b
@[simp]
theorem List.dlookup_cons_ne {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) :
a s.fstdlookup a (s :: l) = dlookup a l
theorem List.dlookup_isSome {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
theorem List.dlookup_eq_none {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
theorem List.of_mem_dlookup {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
b dlookup a la, b l
theorem List.mem_dlookup {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : a, b l) :
b dlookup a l
theorem List.map_dlookup_eq_find {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
Option.map (Sigma.mk a) (dlookup a l) = find? (fun (s : Sigma β) => decide (a = s.fst)) l
theorem List.mem_dlookup_iff {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) :
b dlookup a l a, b l
theorem List.perm_dlookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) :
dlookup a l₁ = dlookup a l₂
theorem List.lookup_ext {α : Type u} {β : αType v} [DecidableEq α] {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys) (h : ∀ (x : α) (y : β x), y dlookup x l₀ y dlookup x l₁) :
l₀.Perm l₁
theorem List.dlookup_map {α : Type u} {α' : Type u'} {β : αType v} {β' : α'Type v'} [DecidableEq α] [DecidableEq α'] (l : List (Sigma β)) {f : αα'} (hf : Function.Injective f) (g : (a : α) → β aβ' (f a)) (a : α) :
dlookup (f a) (map (fun (x : Sigma β) => f x.fst, g x.fst x.snd) l) = Option.map (g a) (dlookup a l)
theorem List.dlookup_map₁ {α : Type u} {α' : Type u'} [DecidableEq α] [DecidableEq α'] {β : Type v} (l : List ((_ : α) × β)) {f : αα'} (hf : Function.Injective f) (a : α) :
dlookup (f a) (map (fun (x : (_ : α) × β) => f x.fst, x.snd) l) = dlookup a l
theorem List.dlookup_map₂ {α : Type u} [DecidableEq α] {γ : αType u_1} {δ : αType u_2} {l : List ((a : α) × γ a)} {f : (a : α) → γ aδ a} (a : α) :
dlookup a (map (fun (x : (a : α) × γ a) => x.fst, f x.fst x.snd) l) = Option.map (f a) (dlookup a l)

lookupAll #

def List.lookupAll {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
List (Sigma β)List (β a)

lookup_all a l is the list of all values in l corresponding to the key a.

Equations
@[simp]
theorem List.lookupAll_nil {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
@[simp]
theorem List.lookupAll_cons_eq {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) :
lookupAll a (a, b :: l) = b :: lookupAll a l
@[simp]
theorem List.lookupAll_cons_ne {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) :
a s.fstlookupAll a (s :: l) = lookupAll a l
theorem List.lookupAll_eq_nil {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
lookupAll a l = [] ∀ (b : β a), ¬a, b l
theorem List.head?_lookupAll {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.mem_lookupAll {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
b lookupAll a l a, b l
theorem List.lookupAll_sublist {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.lookupAll_length_le_one {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
theorem List.lookupAll_eq_dlookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
theorem List.lookupAll_nodup {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
theorem List.perm_lookupAll {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) :
lookupAll a l₁ = lookupAll a l₂
theorem List.dlookup_append {α : Type u} {β : αType v} [DecidableEq α] (l₁ l₂ : List (Sigma β)) (a : α) :
dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)

kreplace #

def List.kreplace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) :
List (Sigma β)List (Sigma β)

Replaces the first value with key a by b.

Equations
theorem List.kreplace_of_forall_not {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (H : ∀ (b : β a), ¬a, b l) :
kreplace a b l = l
theorem List.kreplace_self {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : a, b l) :
kreplace a b l = l
theorem List.keys_kreplace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) :
(kreplace a b l).keys = l.keys
theorem List.kreplace_nodupKeys {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} :
theorem List.Perm.kreplace {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys) :
l₁.Perm l₂(List.kreplace a b l₁).Perm (List.kreplace a b l₂)

kerase #

def List.kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
List (Sigma β)List (Sigma β)

Remove the first pair with the key a.

Equations
@[simp]
theorem List.kerase_nil {α : Type u} {β : αType v} [DecidableEq α] {a : α} :
@[simp]
theorem List.kerase_cons_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a = s.fst) :
kerase a (s :: l) = l
@[simp]
theorem List.kerase_cons_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a s.fst) :
kerase a (s :: l) = s :: kerase a l
@[simp]
theorem List.kerase_of_notMem_keys {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : ¬a l.keys) :
kerase a l = l
@[deprecated List.kerase_of_notMem_keys (since := "2025-05-23")]
theorem List.kerase_of_not_mem_keys {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : ¬a l.keys) :
kerase a l = l

Alias of List.kerase_of_notMem_keys.

theorem List.kerase_sublist {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
(kerase a l).Sublist l
theorem List.kerase_keys_subset {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.mem_keys_of_mem_keys_kerase {α : Type u} {β : αType v} [DecidableEq α] {a₁ a₂ : α} {l : List (Sigma β)} :
a₁ (kerase a₂ l).keysa₁ l.keys
theorem List.exists_of_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : a l.keys) :
(b : β a), (l₁ : List (Sigma β)), (l₂ : List (Sigma β)), ¬a l₁.keys l = l₁ ++ a, b :: l₂ kerase a l = l₁ ++ l₂
@[simp]
theorem List.mem_keys_kerase_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a₁ a₂ : α} {l : List (Sigma β)} (h : a₁ a₂) :
a₁ (kerase a₂ l).keys a₁ l.keys
theorem List.keys_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l : List (Sigma β)} :
(kerase a l).keys = l.keys.erase a
theorem List.kerase_kerase {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {l : List (Sigma β)} :
kerase a (kerase a' l) = kerase a' (kerase a l)
theorem List.NodupKeys.kerase {α : Type u} {β : αType v} {l : List (Sigma β)} [DecidableEq α] (a : α) :
theorem List.Perm.kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys) :
l₁.Perm l₂(List.kerase a l₁).Perm (List.kerase a l₂)
@[simp]
theorem List.notMem_keys_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) :
¬a (kerase a l).keys
@[deprecated List.notMem_keys_kerase (since := "2025-05-23")]
theorem List.not_mem_keys_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) :
¬a (kerase a l).keys

Alias of List.notMem_keys_kerase.

@[simp]
theorem List.dlookup_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) :
@[simp]
theorem List.dlookup_kerase_ne {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {l : List (Sigma β)} (h : a a') :
dlookup a (kerase a' l) = dlookup a l
theorem List.kerase_append_left {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} :
a l₁.keyskerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂
theorem List.kerase_append_right {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} :
¬a l₁.keyskerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
theorem List.kerase_comm {α : Type u} {β : αType v} [DecidableEq α] (a₁ a₂ : α) (l : List (Sigma β)) :
kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)
theorem List.sizeOf_kerase {α : Type u} {β : αType v} [DecidableEq α] [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) :

kinsert #

def List.kinsert {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) :
List (Sigma β)

Insert the pair ⟨a, b⟩ and erase the first pair with the key a.

Equations
@[simp]
theorem List.kinsert_def {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
kinsert a b l = a, b :: kerase a l
theorem List.mem_keys_kinsert {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {b' : β a'} {l : List (Sigma β)} :
a (kinsert a' b' l).keys a = a' a l.keys
theorem List.kinsert_nodupKeys {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (nd : l.NodupKeys) :
theorem List.Perm.kinsert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁.Perm l₂) :
(List.kinsert a b l₁).Perm (List.kinsert a b l₂)
theorem List.dlookup_kinsert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} (l : List (Sigma β)) :
dlookup a (kinsert a b l) = some b
theorem List.dlookup_kinsert_ne {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {b' : β a'} {l : List (Sigma β)} (h : a a') :
dlookup a (kinsert a' b' l) = dlookup a l

kextract #

def List.kextract {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
List (Sigma β)Option (β a) × List (Sigma β)

Finds the first entry with a given key a and returns its value (as an Option because there might be no entry with key a) alongside with the rest of the entries.

Equations
@[simp]
theorem List.kextract_eq_dlookup_kerase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :

dedupKeys #

def List.dedupKeys {α : Type u} {β : αType v} [DecidableEq α] :
List (Sigma β)List (Sigma β)

Remove entries with duplicate keys from l : List (Sigma β).

Equations
theorem List.dedupKeys_cons {α : Type u} {β : αType v} [DecidableEq α] {x : Sigma β} (l : List (Sigma β)) :
theorem List.nodupKeys_dedupKeys {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) :
theorem List.dlookup_dedupKeys {α : Type u} {β : αType v} [DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.sizeOf_dedupKeys {α : Type u} {β : αType v} [DecidableEq α] [SizeOf (Sigma β)] (xs : List (Sigma β)) :

kunion #

def List.kunion {α : Type u} {β : αType v} [DecidableEq α] :
List (Sigma β)List (Sigma β)List (Sigma β)

kunion l₁ l₂ is the append to l₁ of l₂ after, for each key in l₁, the first matching pair in l₂ is erased.

Equations
@[simp]
theorem List.nil_kunion {α : Type u} {β : αType v} [DecidableEq α] {l : List (Sigma β)} :
[].kunion l = l
@[simp]
theorem List.kunion_nil {α : Type u} {β : αType v} [DecidableEq α] {l : List (Sigma β)} :
l.kunion [] = l
@[simp]
theorem List.kunion_cons {α : Type u} {β : αType v} [DecidableEq α] {s : Sigma β} {l₁ l₂ : List (Sigma β)} :
(s :: l₁).kunion l₂ = s :: l₁.kunion (kerase s.fst l₂)
@[simp]
theorem List.mem_keys_kunion {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} :
a (l₁.kunion l₂).keys a l₁.keys a l₂.keys
@[simp]
theorem List.kunion_kerase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} :
(kerase a l₁).kunion (kerase a l₂) = kerase a (l₁.kunion l₂)
theorem List.NodupKeys.kunion {α : Type u} {β : αType v} {l₁ l₂ : List (Sigma β)} [DecidableEq α] (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) :
(l₁.kunion l₂).NodupKeys
theorem List.Perm.kunion_right {α : Type u} {β : αType v} [DecidableEq α] {l₁ l₂ : List (Sigma β)} (p : l₁.Perm l₂) (l : List (Sigma β)) :
(l₁.kunion l).Perm (l₂.kunion l)
theorem List.Perm.kunion_left {α : Type u} {β : αType v} [DecidableEq α] (l : List (Sigma β)) {l₁ l₂ : List (Sigma β)} :
l₁.NodupKeysl₁.Perm l₂(l.kunion l₁).Perm (l.kunion l₂)
theorem List.Perm.kunion {α : Type u} {β : αType v} [DecidableEq α] {l₁ l₂ l₃ l₄ : List (Sigma β)} (nd₃ : l₃.NodupKeys) (p₁₂ : l₁.Perm l₂) (p₃₄ : l₃.Perm l₄) :
(l₁.kunion l₃).Perm (l₂.kunion l₄)
@[simp]
theorem List.dlookup_kunion_left {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} (h : a l₁.keys) :
dlookup a (l₁.kunion l₂) = dlookup a l₁
@[simp]
theorem List.dlookup_kunion_right {α : Type u} {β : αType v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} (h : ¬a l₁.keys) :
dlookup a (l₁.kunion l₂) = dlookup a l₂
theorem List.mem_dlookup_kunion {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} :
b dlookup a (l₁.kunion l₂) b dlookup a l₁ ¬a l₁.keys b dlookup a l₂
@[simp]
theorem List.dlookup_kunion_eq_some {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} :
dlookup a (l₁.kunion l₂) = some b dlookup a l₁ = some b ¬a l₁.keys dlookup a l₂ = some b
theorem List.mem_dlookup_kunion_middle {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ l₃ : List (Sigma β)} (h₁ : b dlookup a (l₁.kunion l₃)) (h₂ : ¬a l₂.keys) :
b dlookup a ((l₁.kunion l₂).kunion l₃)