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 the n-ary section of data.set.basic. 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.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) :
set.image2 m s t ∈ 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 (λ (p : α × β), m p.fst p.snd) (f ×ᶠ 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 ×ᶠ 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 ∈ 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 β} :
filter.map₂ m ⊥ g = ⊥
@[simp]
theorem
filter.map₂_bot_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f : filter α} :
filter.map₂ m f ⊥ = ⊥
@[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) :
(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 (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 (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 (pure a) (pure b) = 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 α × β × γ → δ.
Equations
- filter.map₃ m f g h = {sets := {s : set δ | ∃ (u : set α) (v : set β) (w : set γ), u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ set.image3 m u v w ⊆ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}
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)) :
filter.map₂ m (filter.map₂ n f g) h = filter.map₂ m' f (filter.map₂ n' g h)
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) :
filter.map₂ m f g = filter.map₂ n g f
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 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)) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' f (filter.map n' g)
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)) :
filter.map₂ m (filter.map n f) g = filter.map n' (filter.map₂ m' f g)
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)) :
filter.map₂ m f (filter.map n g) = filter.map n' (filter.map₂ m' f g)
Symmetric of filter.map_map₂_distrib_right.
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 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)) :
filter.map n (filter.map₂ m f g) = filter.map₂ m' g (filter.map n' f)
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)) :
filter.map₂ m (filter.map n f) g = filter.map n' (filter.map₂ m' g f)
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)) :
filter.map₂ m f (filter.map n g) = filter.map n' (filter.map₂ m' g f)
Symmetric of filter.map_map₂_antidistrib_right.