Documentation

Mathlib.Order.Filter.NAry

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 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 β) :

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) :
    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.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₂_eq_bot_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : αβγ} {f : Filter α} {g : Filter β} :
    @[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₂_neBot_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : αβγ} {f : Filter α} {g : Filter β} :
    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) :
    instance Filter.map₂.neBot {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : αβγ} {f : Filter α} {g : Filter β} [Filter.NeBot f] [Filter.NeBot g] :
    Equations
    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 β) :
    @[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 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)) :
    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 β) :
    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.