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.
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_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
- One or more equations did not get rendered due to their size.
Instances For
@[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 ∈ 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)
:
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 (fun (p : α × β) => m p.1 p.2) (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₂ (fun (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 ×ˢ g
theorem
Filter.map₂_mono
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f₁ : Filter α}
{f₂ : Filter α}
{g₁ : Filter β}
{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₁ : Filter β}
{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₁ : Filter α}
{f₂ : Filter α}
{g : Filter β}
(h : f₁ ≤ f₂)
:
Filter.map₂ m f₁ g ≤ Filter.map₂ m f₂ g
@[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₂_neBot_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f : Filter α}
{g : Filter β}
:
Filter.NeBot (Filter.map₂ m f g) ↔ Filter.NeBot f ∧ Filter.NeBot g
theorem
Filter.NeBot.map₂
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f : Filter α}
{g : Filter β}
(hf : Filter.NeBot f)
(hg : Filter.NeBot g)
:
Filter.NeBot (Filter.map₂ m f g)
instance
Filter.map₂.neBot
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f : Filter α}
{g : Filter β}
[Filter.NeBot f]
[Filter.NeBot g]
:
Filter.NeBot (Filter.map₂ m f g)
Equations
- (_ : Filter.NeBot (Filter.map₂ m f g)) = (_ : Filter.NeBot (Filter.map₂ m f g))
theorem
Filter.NeBot.of_map₂_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f : Filter α}
{g : Filter β}
(h : Filter.NeBot (Filter.map₂ m f g))
:
theorem
Filter.NeBot.of_map₂_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f : Filter α}
{g : Filter β}
(h : Filter.NeBot (Filter.map₂ m f g))
:
theorem
Filter.map₂_sup_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{m : α → β → γ}
{f₁ : Filter α}
{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₁ : Filter β}
{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₁ : Filter α}
{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₁ : Filter β}
{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 (m a) 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 (fun (x : α) => m x 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₂ (fun (a : β) (b : α) => m b a) g f
@[simp]
theorem
Filter.map₂_left
{α : Type u_1}
{β : Type u_3}
{f : Filter α}
{g : Filter β}
[Filter.NeBot g]
:
Filter.map₂ (fun (x : α) (x_1 : β) => x) f g = f
@[simp]
theorem
Filter.map₂_right
{α : Type u_1}
{β : Type u_3}
{f : Filter α}
{g : Filter β}
[Filter.NeBot f]
:
Filter.map₂ (fun (x : α) (y : β) => y) f g = g
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₂ (fun (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₂ (fun (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₂ (fun (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 ×ˢ 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 ×ˢ 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 CommSemigroup.
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 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 (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 (pure b) = l
If b is a right identity for f : α → β → α, then pure b is a right identity for
Filter.map₂ f.