feat(data/option/n_ary): Binary map of options (#16763)

Define `option.map₂`, the binary map of options.

src/data/finset/functor.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Scott Morrison
 -/
 import data.finset.lattice
+import data.finset.n_ary
 import data.multiset.functor
 
 /-!
@@ -64,6 +65,12 @@ instance : applicative finset :=
 @[simp] lemma seq_left_def (s : finset α) (t : finset β)  : s <* t = if t = ∅ then ∅ else s := rfl
 @[simp] lemma seq_right_def (s : finset α) (t : finset β)  : s *> t = if s = ∅ then ∅ else t := rfl
 
+/-- `finset.image₂` in terms of monadic operations. Note that this can't be taken as the definition
+because of the lack of universe polymorphism. -/
+lemma image₂_def {α β γ : Type*} (f : α → β → γ) (s : finset α) (t : finset β) :
+  image₂ f s t = f <$> s <*> t :=
+by { ext, simp [mem_sup] }
+
 instance : is_lawful_applicative finset :=
 { seq_left_eq := λ α β s t, begin
     rw [seq_def, fmap_def, seq_left_def],

src/data/finset/n_ary.lean

@@ -13,8 +13,8 @@ This file defines `finset.image₂`, the binary image of finsets. This is the fi
 
 ## Notes
 
-This file is very similar to the n-ary section of `data.set.basic` and to `order.filter.n_ary`.
-Please keep them in sync.
+This file is very similar to the n-ary section of `data.set.basic`, to `order.filter.n_ary` and to
+`data.option.n_ary`. Please keep them in sync.
 
 We do not define `finset.image₃` as its only purpose would be to prove properties of `finset.image₂`
 and `set.image2` already fulfills this task.
@@ -206,6 +206,17 @@ lemma image₂_swap (f : α → β → γ) (s : finset α) (t : finset β) :
   image₂ f s t = image₂ (λ a b, f b a) t s :=
 coe_injective $ by { push_cast, exact image2_swap _ _ _ }
 
+@[simp] lemma image₂_mk_eq_product [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
+  image₂ prod.mk s t = s ×ˢ t :=
+by ext; simp [prod.ext_iff]
+
+@[simp] lemma image₂_curry (f : α × β → γ) (s : finset α) (t : finset β) :
+  image₂ (curry f) s t = (s ×ˢ t).image f :=
+by { classical, rw [←image₂_mk_eq_product, image_image₂, curry] }
+
+@[simp] lemma image_uncurry_product (f : α → β → γ) (s : finset α) (t : finset β) :
+  (s ×ˢ t).image (uncurry f) = image₂ f s t := by rw [←image₂_curry, curry_uncurry]
+
 @[simp] lemma image₂_left [decidable_eq α] (h : t.nonempty) : image₂ (λ x y, x) s t = s :=
 coe_injective $ by { push_cast, exact image2_left h }
 
@@ -235,25 +246,25 @@ lemma image_image₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : 
   (image₂ f s t).image g = image₂ f' (s.image g₁) (t.image g₂) :=
 coe_injective $ by { push_cast, exact image_image2_distrib h_distrib }
 
-/-- Symmetric of `finset.image₂_image_left_comm`. -/
+/-- Symmetric statement to `finset.image₂_image_left_comm`. -/
 lemma image_image₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
   (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
   (image₂ f s t).image g = image₂ f' (s.image g') t :=
 coe_injective $ by { push_cast, exact image_image2_distrib_left h_distrib }
 
-/-- Symmetric of `finset.image_image₂_right_comm`. -/
+/-- Symmetric statement to `finset.image_image₂_right_comm`. -/
 lemma image_image₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
   (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
   (image₂ f s t).image g = image₂ f' s (t.image g') :=
 coe_injective $ by { push_cast, exact image_image2_distrib_right h_distrib }
 
-/-- Symmetric of `finset.image_image₂_distrib_left`. -/
+/-- Symmetric statement to `finset.image_image₂_distrib_left`. -/
 lemma image₂_image_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
   (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
   image₂ f (s.image g) t = (image₂ f' s t).image g' :=
 (image_image₂_distrib_left $ λ a b, (h_left_comm a b).symm).symm
 
-/-- Symmetric of `finset.image_image₂_distrib_right`. -/
+/-- Symmetric statement to `finset.image_image₂_distrib_right`. -/
 lemma image_image₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
   (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
   image₂ f s (t.image g) = (image₂ f' s t).image g' :=
@@ -278,25 +289,25 @@ lemma image_image₂_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁
   (image₂ f s t).image g = image₂ f' (t.image g₁) (s.image g₂) :=
 by { rw image₂_swap f, exact image_image₂_distrib (λ _ _, h_antidistrib _ _) }
 
-/-- Symmetric of `finset.image₂_image_left_anticomm`. -/
+/-- Symmetric statement to `finset.image₂_image_left_anticomm`. -/
 lemma image_image₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
   (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
   (image₂ f s t).image g = image₂ f' (t.image g') s :=
 coe_injective $ by { push_cast, exact image_image2_antidistrib_left h_antidistrib }
 
-/-- Symmetric of `finset.image_image₂_right_anticomm`. -/
+/-- Symmetric statement to `finset.image_image₂_right_anticomm`. -/
 lemma image_image₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
   (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
   (image₂ f s t).image g = image₂ f' t (s.image g') :=
 coe_injective $ by { push_cast, exact image_image2_antidistrib_right h_antidistrib }
 
-/-- Symmetric of `finset.image_image₂_antidistrib_left`. -/
+/-- Symmetric statement to `finset.image_image₂_antidistrib_left`. -/
 lemma image₂_image_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
   (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
   image₂ f (s.image g) t = (image₂ f' t s).image g' :=
 (image_image₂_antidistrib_left $ λ a b, (h_left_anticomm b a).symm).symm
 
-/-- Symmetric of `finset.image_image₂_antidistrib_right`. -/
+/-- Symmetric statement to `finset.image_image₂_antidistrib_right`. -/
 lemma image_image₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
   (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
   image₂ f s (t.image g) = (image₂ f' t s).image g' :=

src/data/option/basic.lean

@@ -35,8 +35,10 @@ namespace option
 variables {α β γ δ : Type*}
 
 lemma coe_def : (coe : α → option α) = some := rfl
+lemma some_eq_coe (a : α) : some a = a := rfl
 
 lemma some_ne_none (x : α) : some x ≠ none := λ h, option.no_confusion h
+@[simp] lemma coe_ne_none (a : α) : (a : option α) ≠ none .
 
 protected lemma «forall» {p : option α → Prop} : (∀ x, p x) ↔ p none ∧ ∀ x, p (some x) :=
 ⟨λ h, ⟨h _, λ x, h _⟩, λ h x, option.cases_on x h.1 h.2⟩

src/data/option/n_ary.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.option.basic
+
+/-!
+# Binary map of options
+
+This file defines the binary map of `option`. This is mostly useful to define pointwise operations
+on intervals.
+
+## Main declarations
+
+* `option.map₂`: Binary map of options.
+
+## Notes
+
+This file is very similar to the n-ary section of `data.set.basic`, to `data.finset.n_ary` and to
+`order.filter.n_ary`. Please keep them in sync.
+
+We do not define `option.map₃` as its only purpose so far would be to prove properties of
+`option.map₂` and casing already fulfills this task.
+-/
+
+open function
+
+namespace option
+variables {α α' β β' γ γ' δ δ' ε ε' : Type*} {f : α → β → γ} {a : option α} {b : option β}
+  {c : option γ}
+
+/-- The image of a binary function `f : α → β → γ` as a function `option α → option β → option γ`.
+Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
+def map₂ (f : α → β → γ) (a : option α) (b : option β) : option γ := a.bind $ λ a, b.map $ f a
+
+/-- `option.map₂` in terms of monadic operations. Note that this can't be taken as the definition
+because of the lack of universe polymorphism. -/
+lemma map₂_def {α β γ : Type*} (f : α → β → γ) (a : option α) (b : option β) :
+  map₂ f a b = f <$> a <*> b := by cases a; refl
+
+@[simp] lemma map₂_some_some (f : α → β → γ) (a : α) (b : β) : map₂ f (some a) (some b) = f a b :=
+rfl
+lemma map₂_coe_coe (f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b := rfl
+@[simp] lemma map₂_none_left (f : α → β → γ) (b : option β) : map₂ f none b = none := rfl
+@[simp] lemma map₂_none_right (f : α → β → γ) (a : option α) : map₂ f a none = none :=
+by cases a; refl
+@[simp] lemma map₂_coe_left (f : α → β → γ) (a : α) (b : option β) :
+  map₂ f a b = b.map (λ b, f a b) := rfl
+@[simp] lemma map₂_coe_right (f : α → β → γ) (a : option α) (b : β) :
+  map₂ f a b = a.map (λ a, f a b) := rfl
+
+@[simp] lemma mem_map₂_iff {c : γ} : c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c :=
+by simp [map₂]
+
+@[simp] lemma map₂_eq_none_iff : map₂ f a b = none ↔ a = none ∨ b = none :=
+by cases a; cases b; simp
+
+lemma map₂_swap (f : α → β → γ) (a : option α) (b : option β) :
+  map₂ f a b = map₂ (λ a b, f b a) b a :=
+by cases a; cases b; refl
+
+lemma map_map₂ (f : α → β → γ) (g : γ → δ) : (map₂ f a b).map g = map₂ (λ a b, g (f a b)) a b :=
+by cases a; cases b; refl
+
+lemma map₂_map_left (f : γ → β → δ) (g : α → γ) :
+  map₂ f (a.map g) b = map₂ (λ a b, f (g a) b) a b :=
+by cases a; refl
+
+lemma map₂_map_right (f : α → γ → δ) (g : β → γ) :
+  map₂ f a (b.map g) = map₂ (λ a b, f a (g b)) a b :=
+by cases b; refl
+
+@[simp] lemma map₂_curry (f : α × β → γ) (a : option α) (b : option β) :
+  map₂ (curry f) a b = option.map f (map₂ prod.mk a b) := (map_map₂ _ _).symm
+
+@[simp] lemma map_uncurry (f : α → β → γ) (x : option (α × β)) :
+  x.map (uncurry f) = map₂ f (x.map prod.fst) (x.map prod.snd) := by cases x; refl
+
+/-!
+### Algebraic replacement rules
+
+A collection of lemmas to transfer associativity, commutativity, distributivity, ... of operations
+to the associativity, commutativity, distributivity, ... of `option.map₂` of those operations.
+The proof pattern is `map₂_lemma operation_lemma`. For example, `map₂_comm mul_comm` proves that
+`map₂ (*) a b = map₂ (*) g f` in a `comm_semigroup`.
+-/
+
+lemma map₂_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
+  (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) :
+  map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c) :=
+by cases a; cases b; cases c; simp [h_assoc]
+
+lemma map₂_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : map₂ f a b = map₂ g b a :=
+by cases a; cases b; simp [h_comm]
+
+lemma map₂_left_comm {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
+  (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) :
+  map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c) :=
+by cases a; cases b; cases c; simp [h_left_comm]
+
+lemma map₂_right_comm {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε}
+  (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) :
+  map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b :=
+by cases a; cases b; cases c; simp [h_right_comm]
+
+lemma map_map₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
+  (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
+  (map₂ f a b).map g = map₂ f' (a.map g₁) (b.map g₂) :=
+by cases a; cases b; simp [h_distrib]
+
+/-!
+The following symmetric restatement are needed because unification has a hard time figuring all the
+functions if you symmetrize on the spot. This is also how the other n-ary APIs do it.
+-/
+
+/-- Symmetric statement to `option.map₂_map_left_comm`. -/
+lemma map_map₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
+  (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
+  (map₂ f a b).map g = map₂ f' (a.map g') b :=
+by cases a; cases b; simp [h_distrib]
+
+/-- Symmetric statement to `option.map_map₂_right_comm`. -/
+lemma map_map₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
+  (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
+  (map₂ f a b).map g = map₂ f' a (b.map g') :=
+by cases a; cases b; simp [h_distrib]
+
+/-- Symmetric statement to `option.map_map₂_distrib_left`. -/
+lemma map₂_map_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
+  (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
+  map₂ f (a.map g) b = (map₂ f' a b).map g' :=
+by cases a; cases b; simp [h_left_comm]
+
+/-- Symmetric statement to `option.map_map₂_distrib_right`. -/
+lemma map_map₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
+  (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
+  map₂ f a (b.map g) = (map₂ f' a b).map g' :=
+by cases a; cases b; simp [h_right_comm]
+
+lemma map_map₂_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
+  (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
+  (map₂ f a b).map g = map₂ f' (b.map g₁) (a.map g₂) :=
+by cases a; cases b; simp [h_antidistrib]
+
+/-- Symmetric statement to `option.map₂_map_left_anticomm`. -/
+lemma map_map₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
+  (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
+  (map₂ f a b).map g = map₂ f' (b.map g') a :=
+by cases a; cases b; simp [h_antidistrib]
+
+/-- Symmetric statement to `option.map_map₂_right_anticomm`. -/
+lemma map_map₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
+  (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
+  (map₂ f a b).map g = map₂ f' b (a.map g') :=
+by cases a; cases b; simp [h_antidistrib]
+
+/-- Symmetric statement to `option.map_map₂_antidistrib_left`. -/
+lemma map₂_map_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
+  (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
+  map₂ f (a.map g) b = (map₂ f' b a).map g' :=
+by cases a; cases b; simp [h_left_anticomm]
+
+/-- Symmetric statement to `option.map_map₂_antidistrib_right`. -/
+lemma map_map₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
+  (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
+  map₂ f a (b.map g) = (map₂ f' b a).map g' :=
+by cases a; cases b; simp [h_right_anticomm]
+
+end option

src/data/set/basic.lean

@@ -2636,7 +2636,8 @@ end image_preimage
 /-!
 ### Images of binary and ternary functions
 
-This section is very similar to `order.filter.n_ary`. Please keep them in sync.
+This section is very similar to `order.filter.n_ary`, `data.finset.n_ary`, `data.option.n_ary`.
+Please keep them in sync.
 -/
 
 section n_ary_image
@@ -2834,25 +2835,25 @@ lemma image_image2_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α
   (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂) :=
 by simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]
 
-/-- Symmetric of `set.image2_image_left_comm`. -/
+/-- Symmetric statement to `set.image2_image_left_comm`. -/
 lemma image_image2_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
   (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
   (image2 f s t).image g = image2 f' (s.image g') t :=
 (image_image2_distrib h_distrib).trans $ by rw image_id'
 
-/-- Symmetric of `set.image_image2_right_comm`. -/
+/-- Symmetric statement to `set.image_image2_right_comm`. -/
 lemma image_image2_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
   (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
   (image2 f s t).image g = image2 f' s (t.image g') :=
 (image_image2_distrib h_distrib).trans $ by rw image_id'
 
-/-- Symmetric of `set.image_image2_distrib_left`. -/
+/-- Symmetric statement to `set.image_image2_distrib_left`. -/
 lemma image2_image_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
   (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
   image2 f (s.image g) t = (image2 f' s t).image g' :=
 (image_image2_distrib_left $ λ a b, (h_left_comm a b).symm).symm
 
-/-- Symmetric of `set.image_image2_distrib_right`. -/
+/-- Symmetric statement to `set.image_image2_distrib_right`. -/
 lemma image_image2_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
   (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
   image2 f s (t.image g) = (image2 f' s t).image g' :=
@@ -2883,25 +2884,25 @@ lemma image_image2_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ :
   (image2 f s t).image g = image2 f' (t.image g₁) (s.image g₂) :=
 by { rw image2_swap f, exact image_image2_distrib (λ _ _, h_antidistrib _ _) }
 
-/-- Symmetric of `set.image2_image_left_anticomm`. -/
+/-- Symmetric statement to `set.image2_image_left_anticomm`. -/
 lemma image_image2_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
   (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
   (image2 f s t).image g = image2 f' (t.image g') s :=
 (image_image2_antidistrib h_antidistrib).trans $ by rw image_id'
 
-/-- Symmetric of `set.image_image2_right_anticomm`. -/
+/-- Symmetric statement to `set.image_image2_right_anticomm`. -/
 lemma image_image2_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
   (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
   (image2 f s t).image g = image2 f' t (s.image g') :=
 (image_image2_antidistrib h_antidistrib).trans $ by rw image_id'
 
-/-- Symmetric of `set.image_image2_antidistrib_left`. -/
+/-- Symmetric statement to `set.image_image2_antidistrib_left`. -/
 lemma image2_image_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
   (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
   image2 f (s.image g) t = (image2 f' t s).image g' :=
 (image_image2_antidistrib_left $ λ a b, (h_left_anticomm b a).symm).symm
 
-/-- Symmetric of `set.image_image2_antidistrib_right`. -/
+/-- Symmetric statement to `set.image_image2_antidistrib_right`. -/
 lemma image_image2_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
   (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
   image2 f s (t.image g) = (image2 f' t s).image g' :=

src/data/set/functor.lean

@@ -29,6 +29,12 @@ instance : monad.{u} set :=
 @[simp] lemma seq_eq_set_seq (s : set (α → β)) (t : set α) : s <*> t = s.seq t := rfl
 @[simp] lemma pure_def (a : α) : (pure a : set α) = {a} := rfl
 
+/-- `set.image2` in terms of monadic operations. Note that this can't be taken as the definition
+because of the lack of universe polymorphism. -/
+lemma image2_def {α β γ : Type*} (f : α → β → γ) (s : set α) (t : set β) :
+  image2 f s t = f <$> s <*> t :=
+by { ext, simp }
+
 instance : is_lawful_monad set :=
 { id_map                := λ α, image_id,
   comp_map              := λ α β γ f g s, image_comp _ _ _,

src/data/set/prod.lean

@@ -281,6 +281,13 @@ set.ext $ λ a,
 
 @[simp] lemma image2_mk_eq_prod : image2 prod.mk s t = s ×ˢ t := ext $ by simp
 
+@[simp] lemma image2_curry (f : α × β → γ) (s : set α) (t : set β) :
+  image2 (λ a b, f (a, b)) s t = (s ×ˢ t).image f :=
+by rw [←image2_mk_eq_prod, image_image2]
+
+@[simp] lemma image_uncurry_prod (f : α → β → γ) (s : set α) (t : set β) :
+  uncurry f '' s ×ˢ t = image2 f s t := by { rw ←image2_curry, refl }
+
 section mono
 
 variables [preorder α] {f : α → set β} {g : α → set γ}