mathlib3 documentation

order.filter.n_ary

N-ary maps of filter #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 data.set.n_ary, data.finset.n_ary and data.option.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
@[simp]
theorem filter.map₂_mk_eq_prod {α : Type u_1} {β : Type u_3} (f : filter α) (g : filter β) :
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 g set.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
@[simp]
theorem filter.map₂_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α × β γ) (f : filter α) (g : filter β) :
@[simp]
theorem filter.map_uncurry_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α β γ) (f : filter α) (g : filter β) :

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 statement to 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 statement to 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 statement to 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 statement to 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 statement to 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 statement to 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 statement to 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 statement to filter.map_map₂_antidistrib_right.

theorem filter.map₂_left_identity {α : Type u_1} {β : Type u_3} {f : α β β} {a : α} (h : (b : β), f a b = b) (l : filter β) :

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_3} {f : α β α} {b : β} (h : (a : α), f a b = a) (l : filter α) :

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