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 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.

@[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 t, 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.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₂ (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 ∈ 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₂_eq_bot_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} : Filter.map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

@[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)

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)) : Filter.NeBot f

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)) : Filter.NeBot 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 (fun 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 (fun 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₂ (fun a b => m b a) g f

@[simp]

theorem Filter.map₂_left {α : Type u_1} {β : Type u_3} {f : Filter α} {g : Filter β} (h : 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 β} (h : Filter.NeBot f) : Filter.map₂ (fun 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

• One or more equations did not get rendered due to their size.

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₃ (fun 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₃ (fun 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₂ (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.