mathlib documentation

order.filter.n_ary

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 #

Notes #

This file is very similar to the n-ary section of data.set.basic and to data.finset.n_ary. Please keep them in sync.

def filter.map₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : filter α) (g : filter β) :

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

Equations
@[simp]
theorem filter.mem_map₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} {u : set γ} :
u filter.map₂ m f g ∃ (s : set α) (t : set β), s f t g set.image2 m s t u
theorem filter.image2_mem_map₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} {s : set α} {t : set β} (hs : s f) (ht : t g) :
theorem filter.map_prod_eq_map₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : filter α) (g : filter β) :
filter.map (λ (p : α × β), m p.fst p.snd) (f.prod g) = filter.map₂ m f g
theorem filter.map_prod_eq_map₂' {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α × β → γ) (f : filter α) (g : filter β) :
filter.map m (f.prod g) = filter.map₂ (λ (a : α) (b : β), m (a, b)) f g
theorem filter.map₂_mono {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ f₂) (hg : g₁ g₂) :
filter.map₂ m f₁ g₁ filter.map₂ m f₂ g₂
theorem filter.map₂_mono_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g₁ g₂ : filter β} (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_5} {m : α → β → γ} {f₁ f₂ : filter α} {g : filter β} (h : f₁ f₂) :
filter.map₂ m f₁ g filter.map₂ m f₂ g
@[simp]
theorem filter.le_map₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} {h : filter γ} :
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_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {g : filter β} :
@[simp]
theorem filter.map₂_bot_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} :
@[simp]
theorem filter.map₂_eq_bot_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} :
@[simp]
theorem filter.map₂_ne_bot_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} :
theorem filter.ne_bot.map₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} (hf : f.ne_bot) (hg : g.ne_bot) :
theorem filter.ne_bot.of_map₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} (h : (filter.map₂ m f g).ne_bot) :
theorem filter.ne_bot.of_map₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} (h : (filter.map₂ m f g).ne_bot) :
theorem filter.map₂_sup_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : filter α} {g : filter β} :
filter.map₂ m (f₁ f₂) g = filter.map₂ m f₁ g filter.map₂ m f₂ g
theorem filter.map₂_sup_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g₁ g₂ : filter β} :
filter.map₂ m f (g₁ g₂) = filter.map₂ m f g₁ filter.map₂ m f g₂
theorem filter.map₂_inf_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : filter α} {g : filter β} :
filter.map₂ m (f₁ f₂) g filter.map₂ m f₁ g filter.map₂ m f₂ g
theorem filter.map₂_inf_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g₁ g₂ : filter β} :
filter.map₂ m f (g₁ g₂) filter.map₂ m f g₁ filter.map₂ m f g₂
@[simp]
theorem filter.map₂_pure_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {g : filter β} {a : α} :
filter.map₂ m (has_pure.pure a) g = filter.map (λ (b : β), m a b) g
@[simp]
theorem filter.map₂_pure_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {b : β} :
filter.map₂ m f (has_pure.pure b) = filter.map (λ (a : α), m a b) f
theorem filter.map₂_pure {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {a : α} {b : β} :
theorem filter.map₂_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : filter α) (g : filter β) :
filter.map₂ m f g = filter.map₂ (λ (a : β) (b : α), m b a) g f
@[simp]
theorem filter.map₂_left {α : Type u_1} {β : Type u_3} {f : filter α} {g : filter β} (h : g.ne_bot) :
filter.map₂ (λ (x : α) (y : β), x) f g = f
@[simp]
theorem filter.map₂_right {α : Type u_1} {β : Type u_3} {f : filter α} {g : filter β} (h : f.ne_bot) :
filter.map₂ (λ (x : α) (y : β), y) f g = g
def filter.map₃ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} (m : α → β → γ → δ) (f : filter α) (g : filter β) (h : filter γ) :

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

Equations
theorem filter.map₂_map₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {f : filter α} {g : filter β} {h : filter γ} (m : δ → γ → ε) (n : α → β → δ) :
filter.map₂ m (filter.map₂ n f g) h = filter.map₃ (λ (a : α) (b : β) (c : γ), m (n a b) c) f g h
theorem filter.map₂_map₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {f : filter α} {g : filter β} {h : filter γ} (m : α → δ → ε) (n : β → γ → δ) :
filter.map₂ m f (filter.map₂ n g h) = filter.map₃ (λ (a : α) (b : β) (c : γ), m a (n b c)) f g h
theorem filter.map_map₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : filter α} {g : filter β} (m : α → β → γ) (n : γ → δ) :
filter.map n (filter.map₂ m f g) = filter.map₂ (λ (a : α) (b : β), n (m a b)) f g
theorem filter.map₂_map_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : filter α} {g : filter β} (m : γ → β → δ) (n : α → γ) :
filter.map₂ m (filter.map n f) g = filter.map₂ (λ (a : α) (b : β), m (n a) b) f g
theorem filter.map₂_map_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : filter α} {g : filter β} (m : α → γ → δ) (n : β → γ) :
filter.map₂ m f (filter.map n g) = filter.map₂ (λ (a : α) (b : β), m a (n b)) 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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {f : filter α} {g : filter β} {m : δ → γ → ε} {n : α → β → δ} {m' : α → ε' → ε} {n' : β → γ → ε'} {h : filter γ} (h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)) :
theorem filter.map₂_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : filter α} {g : filter β} {n : β → α → γ} (h_comm : ∀ (a : α) (b : β), m a b = n b a) :
theorem filter.map₂_left_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {f : filter α} {g : filter β} {h : filter γ} {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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {f : filter α} {g : filter β} {h : filter γ} {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_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : filter α} {g : filter β} {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_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : filter α} {g : filter β} {n : γ → δ} {m' : α' → β → δ} {n' : α → α'} (h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n' a) b) :

Symmetric of filter.map₂_map_left_comm.

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

Symmetric of filter.map_map₂_right_comm.

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

Symmetric of filter.map_map₂_distrib_left.

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

Symmetric of filter.map_map₂_distrib_right.

theorem filter.map₂_distrib_le_left {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9} {f : filter α} {g : filter β} {h : filter γ} {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_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {f : filter α} {g : filter β} {h : filter γ} {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_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : filter α} {g : filter β} {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_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : filter α} {g : filter β} {n : γ → δ} {m' : β' → α → δ} {n' : β → β'} (h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n' b) a) :

Symmetric of filter.map₂_map_left_anticomm.

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

Symmetric of filter.map_map₂_right_anticomm.

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

Symmetric of filter.map_map₂_antidistrib_left.

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

Symmetric of filter.map_map₂_antidistrib_right.