# Documentation

Mathlib.Order.Filter.NAry

# N-ary maps of filter #

This file defines the binary and ternary maps of filters. This is mostly useful to define pointwise operations on filters.

## Main declarations #

• Filter.map₂: Binary map of filters.
• Filter.map₃: Ternary map of filters.

## Notes #

This file is very similar to Data.Set.NAry, Data.Finset.NAry and Data.Option.NAry. Please keep them in sync.

def Filter.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : αβγ) (f : ) (g : ) :

The image of a binary function m : α → β → γ→ β → γ→ γ as a function Filter α → Filter β → Filter γ→ Filter β → Filter γ→ Filter γ. Mathematically this should be thought of as the image of the corresponding function α × β → γ× β → γ→ γ.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Filter.mem_map₂_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } {u : Set γ} :
u Filter.map₂ m f g s t, s f t g Set.image2 m s t u
theorem Filter.image2_mem_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : αβγ} {f : } {g : } {s : Set α} {t : Set β} (hs : s f) (ht : t g) :
theorem Filter.map_prod_eq_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : αβγ) (f : ) (g : ) :
Filter.map (fun p => m p.fst p.snd) () = Filter.map₂ m f g
theorem Filter.map_prod_eq_map₂' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × βγ) (f : ) (g : ) :
Filter.map m () = Filter.map₂ (fun a b => m (a, b)) f g
@[simp]
theorem Filter.map₂_mk_eq_prod {α : Type u_1} {β : Type u_2} (f : ) (g : ) :
Filter.map₂ Prod.mk f g =
theorem Filter.map₂_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : αβγ} {f₁ : } {f₂ : } {g₁ : } {g₂ : } (hf : f₁ f₂) (hg : g₁ g₂) :
Filter.map₂ m f₁ g₁ Filter.map₂ m f₂ g₂
theorem Filter.map₂_mono_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} {m : αβγ} {f : } {g₁ : } {g₂ : } (h : g₁ g₂) :
Filter.map₂ m f g₁ Filter.map₂ m f g₂
theorem Filter.map₂_mono_right {α : Type u_1} {β : Type u_3} {γ : Type u_2} {m : αβγ} {f₁ : } {f₂ : } {g : } (h : f₁ f₂) :
Filter.map₂ m f₁ g Filter.map₂ m f₂ g
@[simp]
theorem Filter.le_map₂_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } {h : } :
h Filter.map₂ m f g ∀ ⦃s : Set α⦄, s f∀ ⦃t : Set β⦄, t gSet.image2 m s t h
@[simp]
theorem Filter.map₂_bot_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {g : } :
@[simp]
theorem Filter.map₂_bot_right {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } :
@[simp]
theorem Filter.map₂_eq_bot_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } :
@[simp]
theorem Filter.map₂_neBot_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } :
theorem Filter.NeBot.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : αβγ} {f : } {g : } (hf : ) (hg : ) :
theorem Filter.NeBot.of_map₂_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } (h : Filter.NeBot (Filter.map₂ m f g)) :
theorem Filter.NeBot.of_map₂_right {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } (h : Filter.NeBot (Filter.map₂ m f g)) :
theorem Filter.map₂_sup_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f₁ : } {f₂ : } {g : } :
Filter.map₂ m (f₁ f₂) g = Filter.map₂ m f₁ g Filter.map₂ m f₂ g
theorem Filter.map₂_sup_right {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g₁ : } {g₂ : } :
Filter.map₂ m f (g₁ g₂) = Filter.map₂ m f g₁ Filter.map₂ m f g₂
theorem Filter.map₂_inf_subset_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f₁ : } {f₂ : } {g : } :
Filter.map₂ m (f₁ f₂) g Filter.map₂ m f₁ g Filter.map₂ m f₂ g
theorem Filter.map₂_inf_subset_right {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g₁ : } {g₂ : } :
Filter.map₂ m f (g₁ g₂) Filter.map₂ m f g₁ Filter.map₂ m f g₂
@[simp]
theorem Filter.map₂_pure_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {g : } {a : α} :
Filter.map₂ m (pure a) g = Filter.map (fun b => m a b) g
@[simp]
theorem Filter.map₂_pure_right {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {b : β} :
Filter.map₂ m f (pure b) = Filter.map (fun a => m a b) f
theorem Filter.map₂_pure {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {a : α} {b : β} :
Filter.map₂ m (pure a) (pure b) = pure (m a b)
theorem Filter.map₂_swap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : αβγ) (f : ) (g : ) :
Filter.map₂ m f g = Filter.map₂ (fun a b => m b a) g f
@[simp]
theorem Filter.map₂_left {α : Type u_2} {β : Type u_1} {f : } {g : } (h : ) :
Filter.map₂ (fun x x_1 => x) f g = f
@[simp]
theorem Filter.map₂_right {α : Type u_1} {β : Type u_2} {f : } {g : } (h : ) :
Filter.map₂ (fun x y => y) f g = g
def Filter.map₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (m : αβγδ) (f : ) (g : ) (h : ) :

The image of a ternary function m : α → β → γ → δ→ β → γ → δ→ γ → δ→ δ as a function Filter α → Filter β → Filter γ → Filter δ→ Filter β → Filter γ → Filter δ→ Filter γ → Filter δ→ Filter δ. Mathematically this should be thought of as the image of the corresponding function α × β × γ → δ× β × γ → δ× γ → δ→ δ.

Equations
• One or more equations did not get rendered due to their size.
theorem Filter.map₂_map₂_left {α : Type u_4} {β : Type u_5} {γ : Type u_3} {δ : Type u_2} {ε : Type u_1} {f : } {g : } {h : } (m : δγε) (n : αβδ) :
Filter.map₂ m (Filter.map₂ n f g) h = Filter.map₃ (fun a b c => m (n a b) c) f g h
theorem Filter.map₂_map₂_right {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_3} {ε : Type u_1} {f : } {g : } {h : } (m : αδε) (n : βγδ) :
Filter.map₂ m f (Filter.map₂ n g h) = Filter.map₃ (fun a b c => m a (n b c)) f g h
theorem Filter.map_map₂ {α : Type u_3} {β : Type u_4} {γ : Type u_2} {δ : Type u_1} {f : } {g : } (m : αβγ) (n : γδ) :
Filter.map n (Filter.map₂ m f g) = Filter.map₂ (fun a b => n (m a b)) f g
theorem Filter.map₂_map_left {α : Type u_4} {β : Type u_3} {γ : Type u_2} {δ : Type u_1} {f : } {g : } (m : γβδ) (n : αγ) :
Filter.map₂ m () g = Filter.map₂ (fun a b => m (n a) b) f g
theorem Filter.map₂_map_right {α : Type u_2} {β : Type u_4} {γ : Type u_3} {δ : Type u_1} {f : } {g : } (m : αγδ) (n : βγ) :
Filter.map₂ m f () = Filter.map₂ (fun a b => m a (n b)) f g
@[simp]
theorem Filter.map₂_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × βγ) (f : ) (g : ) :
@[simp]
theorem Filter.map_uncurry_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : αβγ) (f : ) (g : ) :

### Algebraic replacement rules #

A collection of lemmas to transfer associativity, commutativity, distributivity, ... of operations to the associativity, commutativity, distributivity, ... of Filter.map₂ of those operations.

The proof pattern is map₂_lemma operation_lemma. For example, map₂_comm mul_comm proves that map₂ (*) f g = map₂ (*) g f in a comm_semigroup.

theorem Filter.map₂_assoc {α : Type u_4} {β : Type u_5} {γ : Type u_1} {δ : Type u_3} {ε : Type u_2} {ε' : Type u_6} {f : } {g : } {m : δγε} {n : αβδ} {m' : αε'ε} {n' : βγε'} {h : } (h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)) :
theorem Filter.map₂_comm {α : Type u_2} {β : Type u_3} {γ : Type u_1} {m : αβγ} {f : } {g : } {n : βαγ} (h_comm : ∀ (a : α) (b : β), m a b = n b a) :
theorem Filter.map₂_left_comm {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_3} {δ' : Type u_6} {ε : Type u_1} {f : } {g : } {h : } {m : αδε} {n : βγδ} {m' : αγδ'} {n' : βδ'ε} (h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)) :
theorem Filter.map₂_right_comm {α : Type u_4} {β : Type u_5} {γ : Type u_3} {δ : Type u_2} {δ' : Type u_6} {ε : Type u_1} {f : } {g : } {h : } {m : δγε} {n : αβδ} {m' : αγδ'} {n' : δ'βε} (h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b) :
theorem Filter.map_map₂_distrib {α : Type u_3} {α' : Type u_5} {β : Type u_4} {β' : Type u_6} {γ : Type u_2} {δ : Type u_1} {m : αβγ} {f : } {g : } {n : γδ} {m' : α'β'δ} {n₁ : αα'} {n₂ : ββ'} (h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)) :
theorem Filter.map_map₂_distrib_left {α : Type u_3} {α' : Type u_5} {β : Type u_4} {γ : Type u_2} {δ : Type u_1} {m : αβγ} {f : } {g : } {n : γδ} {m' : α'βδ} {n' : αα'} (h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n' a) b) :

Symmetric statement to Filter.map₂_map_left_comm.

theorem Filter.map_map₂_distrib_right {α : Type u_3} {β : Type u_4} {β' : Type u_5} {γ : Type u_2} {δ : Type u_1} {m : αβγ} {f : } {g : } {n : γδ} {m' : αβ'δ} {n' : ββ'} (h_distrib : ∀ (a : α) (b : β), n (m a b) = m' a (n' b)) :

Symmetric statement to Filter.map_map₂_right_comm.

theorem Filter.map₂_map_left_comm {α : Type u_4} {α' : Type u_2} {β : Type u_3} {γ : Type u_1} {δ : Type u_5} {f : } {g : } {m : α'βγ} {n : αα'} {m' : αβδ} {n' : δγ} (h_left_comm : ∀ (a : α) (b : β), m (n a) b = n' (m' a b)) :

Symmetric statement to Filter.map_map₂_distrib_left.

theorem Filter.map_map₂_right_comm {α : Type u_2} {β : Type u_4} {β' : Type u_3} {γ : Type u_1} {δ : Type u_5} {f : } {g : } {m : αβ'γ} {n : ββ'} {m' : αβδ} {n' : δγ} (h_right_comm : ∀ (a : α) (b : β), m a (n b) = n' (m' a b)) :

Symmetric statement to Filter.map_map₂_distrib_right.

theorem Filter.map₂_distrib_le_left {α : Type u_2} {β : Type u_4} {β' : Type u_6} {γ : Type u_5} {γ' : Type u_7} {δ : Type u_3} {ε : Type u_1} {f : } {g : } {h : } {m : αδε} {n : βγδ} {m₁ : αββ'} {m₂ : αγγ'} {n' : β'γ'ε} (h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)) :

The other direction does not hold because of the f-f cross terms on the RHS.

theorem Filter.map₂_distrib_le_right {α : Type u_4} {α' : Type u_6} {β : Type u_5} {β' : Type u_7} {γ : Type u_3} {δ : Type u_2} {ε : Type u_1} {f : } {g : } {h : } {m : δγε} {n : αβδ} {m₁ : αγα'} {m₂ : βγβ'} {n' : α'β'ε} (h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)) :

The other direction does not hold because of the h-h cross terms on the RHS.

theorem Filter.map_map₂_antidistrib {α : Type u_3} {α' : Type u_6} {β : Type u_4} {β' : Type u_5} {γ : Type u_2} {δ : Type u_1} {m : αβγ} {f : } {g : } {n : γδ} {m' : β'α'δ} {n₁ : ββ'} {n₂ : αα'} (h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)) :
theorem Filter.map_map₂_antidistrib_left {α : Type u_3} {β : Type u_4} {β' : Type u_5} {γ : Type u_2} {δ : Type u_1} {m : αβγ} {f : } {g : } {n : γδ} {m' : β'αδ} {n' : ββ'} (h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n' b) a) :

Symmetric statement to Filter.map₂_map_left_anticomm.

theorem Filter.map_map₂_antidistrib_right {α : Type u_3} {α' : Type u_5} {β : Type u_4} {γ : Type u_2} {δ : Type u_1} {m : αβγ} {f : } {g : } {n : γδ} {m' : βα'δ} {n' : αα'} (h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' b (n' a)) :

Symmetric statement to Filter.map_map₂_right_anticomm.

theorem Filter.map₂_map_left_anticomm {α : Type u_4} {α' : Type u_2} {β : Type u_3} {γ : Type u_1} {δ : Type u_5} {f : } {g : } {m : α'βγ} {n : αα'} {m' : βαδ} {n' : δγ} (h_left_anticomm : ∀ (a : α) (b : β), m (n a) b = n' (m' b a)) :

Symmetric statement to Filter.map_map₂_antidistrib_left.

theorem Filter.map_map₂_right_anticomm {α : Type u_2} {β : Type u_4} {β' : Type u_3} {γ : Type u_1} {δ : Type u_5} {f : } {g : } {m : αβ'γ} {n : ββ'} {m' : βαδ} {n' : δγ} (h_right_anticomm : ∀ (a : α) (b : β), m a (n b) = n' (m' b a)) :

Symmetric statement to Filter.map_map₂_antidistrib_right.

theorem Filter.map₂_left_identity {α : Type u_2} {β : Type u_1} {f : αββ} {a : α} (h : ∀ (b : β), f a b = b) (l : ) :
Filter.map₂ f (pure a) l = l

If a is a left identity for f : α → β → β→ β → β→ β, then pure a is a left identity for Filter.map₂ f.

theorem Filter.map₂_right_identity {α : Type u_1} {β : Type u_2} {f : αβα} {b : β} (h : ∀ (a : α), f a b = a) (l : ) :
Filter.map₂ f l (pure b) = l

If b is a right identity for f : α → β → α→ β → α→ α, then pure b is a right identity for Filter.map₂ f.