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 #
filter.map₂: Binary map of filters.filter.map₃: Ternary map of filters.
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 β) :
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
- filter.map₂ m f g = {sets := {s : set γ | ∃ (u : set α) (v : set β), u ∈ f ∧ v ∈ g ∧ set.image2 m u v ⊆ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}
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 β) :
filter.map₂ prod.mk f g = f.prod 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
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 : β} :
filter.map₂ m (has_pure.pure a) (has_pure.pure b) = has_pure.pure (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 γ) :
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 α × β × γ → δ.
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 β) :
filter.map₂ (function.curry m) f g = filter.map m (f.prod g)
@[simp]
theorem
filter.map_uncurry_prod
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
(m : α → β → γ)
(f : filter α)
(g : filter β) :
filter.map (function.uncurry m) (f.prod g) = filter.map₂ 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_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)) :
filter.map₂ m (filter.map₂ n f g) h = filter.map₂ m' f (filter.map₂ n' g h)
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)) :
filter.map₂ m f (filter.map₂ n g h) = filter.map₂ n' g (filter.map₂ m' f h)
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) :
filter.map₂ m (filter.map₂ n f g) h = filter.map₂ n' (filter.map₂ m' f h) g
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)) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' (filter.map n₁ f) (filter.map n₂ g)
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) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' (filter.map n' f) g
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)) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' f (filter.map n' g)
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)) :
filter.map₂ m (filter.map n f) g = filter.map n' (filter.map₂ m' f g)
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)) :
filter.map₂ m f (filter.map n g) = filter.map n' (filter.map₂ m' f g)
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)) :
filter.map₂ m f (filter.map₂ n g h) ≤ filter.map₂ n' (filter.map₂ m₁ f g) (filter.map₂ m₂ f h)
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)) :
filter.map₂ m (filter.map₂ n f g) h ≤ filter.map₂ n' (filter.map₂ m₁ f h) (filter.map₂ m₂ g h)
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)) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' (filter.map n₁ g) (filter.map n₂ f)
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) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' (filter.map n' g) f
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)) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' g (filter.map n' f)
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)) :
filter.map₂ m (filter.map n f) g = filter.map n' (filter.map₂ m' g f)
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)) :
filter.map₂ m f (filter.map n g) = filter.map n' (filter.map₂ m' g f)
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 β) :
filter.map₂ f (has_pure.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_3}
{f : α → β → α}
{b : β}
(h : ∀ (a : α), f a b = a)
(l : filter α) :
filter.map₂ f l (has_pure.pure b) = l
If b is a right identity for f : α → β → α, then pure b is a right identity for
filter.map₂ f.