Mathlib.Order.Filter.NAry

Filter.map₂ definition

(m : α → β → γ) (f : Filter α) (g : Filter β) : Filter γ

Full source

/-- 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 `α × β → γ`. -/
def map₂ (m : α → β → γ) (f : Filter α) (g : Filter β) : Filter γ :=
  ((f ×ˢ g).map (uncurry m)).copy { s | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s } fun _ ↦ by
    simp only [mem_map, mem_prod_iff, image2_subset_iff, prod_subset_iff]; rfl

Binary image filter of a function

Informal description

Given a binary function $ m : \alpha \to \beta \to \gamma $ and filters $ f $ on $ \alpha $ and $ g $ on $ \beta $, the filter $ \text{map}_2 \, m \, f \, g $ on $ \gamma $ is defined as the collection of all subsets $ s \subseteq \gamma $ for which there exist sets $ u \in f $ and $ v \in g $ such that the image $ \{ m(a, b) \mid a \in u, b \in v \} $ is contained in $ s $. This construction can be thought of as the image of the corresponding function $ \alpha \times \beta \to \gamma $ applied to the product filter $ f \times g $.

Filter.mem_map₂_iff theorem

: u ∈ map₂ m f g ↔ ∃ s ∈ f, ∃ t ∈ g, image2 m s t ⊆ u

Full source

@[simp 900]
theorem mem_map₂_iff : u ∈ map₂ m f gu ∈ map₂ m f g ↔ ∃ s ∈ f, ∃ t ∈ g, image2 m s t ⊆ u :=
  Iff.rfl

Characterization of Membership in Binary Image Filter

Informal description

A subset $u$ of $\gamma$ belongs to the binary image filter $\text{map}_2(m, f, g)$ if and only if there exist subsets $s \in f$ and $t \in g$ such that the image $\{m(a, b) \mid a \in s, b \in t\}$ is contained in $u$.

Filter.image2_mem_map₂ theorem

(hs : s ∈ f) (ht : t ∈ g) : image2 m s t ∈ map₂ m f g

Full source

theorem image2_mem_map₂ (hs : s ∈ f) (ht : t ∈ g) : image2image2 m s t ∈ map₂ m f g :=
  ⟨_, hs, _, ht, Subset.rfl⟩

Image of Binary Function Preserves Filter Membership

Informal description

Let $m : \alpha \to \beta \to \gamma$ be a binary function, and let $f$ and $g$ be filters on types $\alpha$ and $\beta$ respectively. If $s \in f$ and $t \in g$, then the image $\text{image2}(m, s, t) \in \text{map}_2(m, f, g)$, where $\text{image2}(m, s, t) = \{m(a, b) \mid a \in s, b \in t\}$.

Filter.map_prod_eq_map₂ theorem

 (m : α → β → γ) (f : Filter α) (g : Filter β) : Filter.map (fun p : α × β => m p.1 p.2) (f ×ˢ g) = map₂ m f g

Full source

theorem map_prod_eq_map₂ (m : α → β → γ) (f : Filter α) (g : Filter β) :
    Filter.map (fun p : α × β => m p.1 p.2) (f ×ˢ g) = map₂ m f g := by
  rw [map₂, copy_eq, uncurry_def]

Equality of Image Filter via Uncurrying and Binary Image Filter: $\text{map}(m \circ \text{uncurry})(f \timesˢ g) = \text{map}_2 \, m \, f \, g$

Informal description

For any binary function $m \colon \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the image filter of the uncurried function $(a, b) \mapsto m(a, b)$ under the product filter $f \timesˢ g$ is equal to the binary image filter $\text{map}_2 \, m \, f \, g$.

Filter.map_prod_eq_map₂' theorem

(m : α × β → γ) (f : Filter α) (g : Filter β) : Filter.map m (f ×ˢ g) = map₂ (fun a b => m (a, b)) f g

Full source

theorem map_prod_eq_map₂' (m : α × β → γ) (f : Filter α) (g : Filter β) :
    Filter.map m (f ×ˢ g) = map₂ (fun a b => m (a, b)) f g :=
  map_prod_eq_map₂ m.curry f g

Equality of Image Filter under Product and Binary Image Filter via Currying

Informal description

For any function $m \colon \alpha \times \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the image filter of $m$ under the product filter $f \timesˢ g$ is equal to the binary image filter of the curried function $(a, b) \mapsto m(a, b)$ applied to $f$ and $g$. That is, \[ \text{map}(m)(f \timesˢ g) = \text{map}_2 (\lambda a \, b, m(a, b)) \, f \, g. \]

Filter.map₂_mk_eq_prod theorem

(f : Filter α) (g : Filter β) : map₂ Prod.mk f g = f ×ˢ g

Full source

@[simp]
theorem map₂_mk_eq_prod (f : Filter α) (g : Filter β) : map₂ Prod.mk f g = f ×ˢ g := by
  simp only [← map_prod_eq_map₂, map_id']

Equivalence of Binary Image Filter and Product Filter for Product Construction

Informal description

For any filters $f$ on type $\alpha$ and $g$ on type $\beta$, the binary image filter of the product constructor $\text{Prod.mk}$ applied to $f$ and $g$ is equal to the product filter $f \timesˢ g$. In other words, $\text{map}_2 \text{Prod.mk} f g = f \timesˢ g$.

Filter.map₂_mono theorem

(hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : map₂ m f₁ g₁ ≤ map₂ m f₂ g₂

Full source

@[gcongr]
theorem map₂_mono (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : map₂ m f₁ g₁ ≤ map₂ m f₂ g₂ :=
  fun _ ⟨s, hs, t, ht, hst⟩ => ⟨s, hf hs, t, hg ht, hst⟩

Monotonicity of Binary Image Filter with Respect to Filter Inclusion

Informal description

Let $m : \alpha \to \beta \to \gamma$ be a binary function, and let $f_1, f_2$ be filters on $\alpha$ and $g_1, g_2$ be filters on $\beta$. If $f_1 \leq f_2$ and $g_1 \leq g_2$, then the binary image filter satisfies $\text{map}_2 \, m \, f_1 \, g_1 \leq \text{map}_2 \, m \, f_2 \, g_2$.

Filter.map₂_mono_left theorem

(h : g₁ ≤ g₂) : map₂ m f g₁ ≤ map₂ m f g₂

Full source

@[gcongr]
theorem map₂_mono_left (h : g₁ ≤ g₂) : map₂ m f g₁ ≤ map₂ m f g₂ :=
  map₂_mono Subset.rfl h

Left Monotonicity of Binary Image Filter with Respect to Filter Inclusion

Informal description

For a binary function $m : \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$, $g_1$, $g_2$ on $\beta$, if $g_1 \leq g_2$, then the binary image filter satisfies $\text{map}_2 \, m \, f \, g_1 \leq \text{map}_2 \, m \, f \, g_2$.

Filter.map₂_mono_right theorem

(h : f₁ ≤ f₂) : map₂ m f₁ g ≤ map₂ m f₂ g

Full source

@[gcongr]
theorem map₂_mono_right (h : f₁ ≤ f₂) : map₂ m f₁ g ≤ map₂ m f₂ g :=
  map₂_mono h Subset.rfl

Monotonicity of Binary Image Filter with Respect to Right Filter Inclusion

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and filters $f_1, f_2$ on $\alpha$ and $g$ on $\beta$, if $f_1 \leq f_2$, then the binary image filter satisfies $\text{map}_2 \, m \, f_1 \, g \leq \text{map}_2 \, m \, f_2 \, g$.

Filter.le_map₂_iff theorem

{h : Filter γ} : h ≤ map₂ m f g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → image2 m s t ∈ h

Full source

@[simp]
theorem le_map₂_iff {h : Filter γ} :
    h ≤ map₂ m f g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → image2 m s t ∈ h :=
  ⟨fun H _ hs _ ht => H <| image2_mem_map₂ hs ht, fun H _ ⟨_, hs, _, ht, hu⟩ =>
    mem_of_superset (H hs ht) hu⟩

Characterization of Filter Refinement via Binary Image Filter

Informal description

For any filter $h$ on a type $\gamma$, a binary function $m : \alpha \to \beta \to \gamma$, and filters $f$ on $\alpha$ and $g$ on $\beta$, the following are equivalent: 1. The filter $h$ is finer than the binary image filter $\text{map}_2(m, f, g)$. 2. For all sets $s \in f$ and $t \in g$, the image $\text{image2}(m, s, t) \in h$. Here, $\text{image2}(m, s, t) = \{m(a, b) \mid a \in s, b \in t\}$.

Filter.map₂_eq_bot_iff theorem

: map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Full source

@[simp]
theorem map₂_eq_bot_iff : map₂map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by simp [← map_prod_eq_map₂]

Binary Image Filter is Bottom iff Either Input is Bottom

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, f \, g$ is equal to the bottom filter $\bot$ if and only if either $f$ is the bottom filter or $g$ is the bottom filter.

Filter.map₂_bot_left theorem

: map₂ m ⊥ g = ⊥

Full source

@[simp]
theorem map₂_bot_left : map₂ m ⊥ g = ⊥ := map₂_eq_bot_iff.2 <| .inl rfl

Binary image filter with left bottom filter is bottom

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and any filter $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, \bot \, g$ is equal to the bottom filter $\bot$.

Filter.map₂_bot_right theorem

: map₂ m f ⊥ = ⊥

Full source

@[simp]
theorem map₂_bot_right : map₂ m f ⊥ = ⊥ := map₂_eq_bot_iff.2 <| .inr rfl

Binary image filter with right bottom filter is bottom

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and filter $f$ on $\alpha$, the binary image filter $\text{map}_2 \, m \, f \, \bot$ is equal to the bottom filter $\bot$.

Filter.map₂_neBot_iff theorem

: (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot

Full source

@[simp]
theorem map₂_neBot_iff : (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot := by simp [neBot_iff, not_or]

Non-triviality condition for binary image filter

Informal description

For a binary function $m : \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the filter $\text{map}_2 \, m \, f \, g$ is non-trivial if and only if both $f$ and $g$ are non-trivial filters.

Filter.NeBot.map₂ theorem

(hf : f.NeBot) (hg : g.NeBot) : (map₂ m f g).NeBot

Full source

protected theorem NeBot.map₂ (hf : f.NeBot) (hg : g.NeBot) : (map₂ m f g).NeBot :=
  map₂_neBot_iff.2 ⟨hf, hg⟩

Non-triviality preservation under binary image filter

Informal description

Given a binary function $m : \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, if both $f$ and $g$ are non-trivial filters, then the binary image filter $\text{map}_2 \, m \, f \, g$ is also non-trivial.

Filter.map₂.neBot instance

[NeBot f] [NeBot g] : NeBot (map₂ m f g)

Full source

instance map₂.neBot [NeBot f] [NeBot g] : NeBot (map₂ m f g) := .map₂ ‹_› ‹_›

Non-triviality of binary image filter under non-trivial filters

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and non-trivial filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, f \, g$ is also non-trivial.

Filter.NeBot.of_map₂_left theorem

(h : (map₂ m f g).NeBot) : f.NeBot

Full source

theorem NeBot.of_map₂_left (h : (map₂ m f g).NeBot) : f.NeBot :=
  (map₂_neBot_iff.1 h).1

Non-triviality of First Filter in Binary Image Filter

Informal description

If the binary image filter $\text{map}_2 \, m \, f \, g$ is non-trivial, then the filter $f$ is also non-trivial.

Filter.NeBot.of_map₂_right theorem

(h : (map₂ m f g).NeBot) : g.NeBot

Full source

theorem NeBot.of_map₂_right (h : (map₂ m f g).NeBot) : g.NeBot :=
  (map₂_neBot_iff.1 h).2

Non-triviality of Right Filter in Binary Image Filter

Informal description

If the binary image filter $\text{map}_2 \, m \, f \, g$ is non-trivial, then the filter $g$ is non-trivial.

Filter.map₂_sup_left theorem

: map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g

Full source

theorem map₂_sup_left : map₂ m (f₁ ⊔ f₂) g = map₂map₂ m f₁ g ⊔ map₂ m f₂ g := by
  simp_rw [← map_prod_eq_map₂, sup_prod, map_sup]

Binary Image Filter Preserves Supremum on Left Filter: $\text{map}_2 \, m \, (f_1 \sqcup f_2) \, g = \text{map}_2 \, m \, f_1 \, g \sqcup \text{map}_2 \, m \, f_2 \, g$

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and filters $f_1, f_2$ on $\alpha$ and $g$ on $\beta$, the binary image filter satisfies: $$\text{map}_2 \, m \, (f_1 \sqcup f_2) \, g = \text{map}_2 \, m \, f_1 \, g \sqcup \text{map}_2 \, m \, f_2 \, g.$$

Filter.map₂_sup_right theorem

: map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Full source

theorem map₂_sup_right : map₂ m f (g₁ ⊔ g₂) = map₂map₂ m f g₁ ⊔ map₂ m f g₂ := by
  simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]

Right Supremum Preservation for Binary Image Filter: $\text{map}_2 \, m \, f \, (g_1 \sqcup g_2) = \text{map}_2 \, m \, f \, g_1 \sqcup \text{map}_2 \, m \, f \, g_2$

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$, any filter $f$ on $\alpha$, and any filters $g_1, g_2$ on $\beta$, the binary image filter satisfies: $$\text{map}_2 \, m \, f \, (g_1 \sqcup g_2) = \text{map}_2 \, m \, f \, g_1 \sqcup \text{map}_2 \, m \, f \, g_2.$$

Filter.map₂_inf_subset_left theorem

: map₂ m (f₁ ⊓ f₂) g ≤ map₂ m f₁ g ⊓ map₂ m f₂ g

Full source

theorem map₂_inf_subset_left : map₂ m (f₁ ⊓ f₂) g ≤ map₂map₂ m f₁ g ⊓ map₂ m f₂ g :=
  Monotone.map_inf_le (fun _ _ ↦ map₂_mono_right) f₁ f₂

Binary Image Filter Preserves Infimum Inequality on Left Filter

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and filters $f_1, f_2$ on $\alpha$ and $g$ on $\beta$, the binary image filter satisfies $\text{map}_2 \, m \, (f_1 \sqcap f_2) \, g \leq \text{map}_2 \, m \, f_1 \, g \sqcap \text{map}_2 \, m \, f_2 \, g$.

Filter.map₂_inf_subset_right theorem

: map₂ m f (g₁ ⊓ g₂) ≤ map₂ m f g₁ ⊓ map₂ m f g₂

Full source

theorem map₂_inf_subset_right : map₂ m f (g₁ ⊓ g₂) ≤ map₂map₂ m f g₁ ⊓ map₂ m f g₂ :=
  Monotone.map_inf_le (fun _ _ ↦ map₂_mono_left) g₁ g₂

Right Infimum Subset Property for Binary Image Filter

Informal description

For any binary function $m : \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$, $g_1$, $g_2$ on $\beta$, the binary image filter satisfies $\text{map}_2 \, m \, f \, (g_1 \sqcap g_2) \leq \text{map}_2 \, m \, f \, g_1 \sqcap \text{map}_2 \, m \, f \, g_2$.

Filter.map₂_pure_left theorem

: map₂ m (pure a) g = g.map (m a)

Full source

@[simp]
theorem map₂_pure_left : map₂ m (pure a) g = g.map (m a) := by
  rw [← map_prod_eq_map₂, pure_prod, map_map]; rfl

Binary Image Filter with Pure Left Argument Equals Image Filter of Right Argument

Informal description

For any binary function $m \colon \alpha \to \beta \to \gamma$, any element $a \in \alpha$, and any filter $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, (\text{pure } a) \, g$ is equal to the image filter of $g$ under the function $m(a) \colon \beta \to \gamma$. In symbols: $$\text{map}_2 \, m \, (\text{pure } a) \, g = \text{map} \, (m(a)) \, g$$

Filter.map₂_pure_right theorem

: map₂ m f (pure b) = f.map (m · b)

Full source

@[simp]
theorem map₂_pure_right : map₂ m f (pure b) = f.map (m · b) := by
  rw [← map_prod_eq_map₂, prod_pure, map_map]; rfl

Binary Image Filter with Right Pure Filter Equals Unary Image Filter

Informal description

For any binary function $m \colon \alpha \to \beta \to \gamma$, any filter $f$ on $\alpha$, and any element $b \in \beta$, the binary image filter $\text{map}_2 \, m \, f \, (\text{pure } b)$ is equal to the image filter of $f$ under the unary function $\lambda a, m(a, b)$.

Filter.map₂_pure theorem

: map₂ m (pure a) (pure b) = pure (m a b)

Full source

theorem map₂_pure : map₂ m (pure a) (pure b) = pure (m a b) := by rw [map₂_pure_right, map_pure]

Binary Image Filter of Pure Filters Equals Pure Filter of Function Application

Informal description

For any binary function $m \colon \alpha \to \beta \to \gamma$ and elements $a \in \alpha$, $b \in \beta$, the binary image filter $\text{map}_2 \, m \, (\text{pure } a) \, (\text{pure } b)$ is equal to the pure filter generated by $\{m(a, b)\}$. In symbols: $$\text{map}_2 \, m \, (\text{pure } a) \, (\text{pure } b) = \text{pure } (m(a, b))$$

Filter.map₂_swap theorem

(m : α → β → γ) (f : Filter α) (g : Filter β) : map₂ m f g = map₂ (fun a b => m b a) g f

Full source

theorem map₂_swap (m : α → β → γ) (f : Filter α) (g : Filter β) :
    map₂ m f g = map₂ (fun a b => m b a) g f := by
  rw [← map_prod_eq_map₂, prod_comm, map_map, ← map_prod_eq_map₂, Function.comp_def]

Commutativity of Binary Image Filter: $\text{map}_2 \, m \, f \, g = \text{map}_2 \, (\text{swap } m) \, g \, f$

Informal description

For any binary function $m \colon \alpha \to \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, f \, g$ is equal to the binary image filter $\text{map}_2 \, (\lambda a b, m b a) \, g \, f$.

Filter.map₂_left theorem

[NeBot g] : map₂ (fun x _ => x) f g = f

Full source

@[simp]
theorem map₂_left [NeBot g] : map₂ (fun x _ => x) f g = f := by
  rw [← map_prod_eq_map₂, map_fst_prod]

Left Projection of Binary Image Filter Equals First Filter

Informal description

For any filter $f$ on a type $\alpha$ and any non-trivial filter $g$ on a type $\beta$, the binary image filter of the projection function $(x, \_) \mapsto x$ applied to $f$ and $g$ equals $f$.

Filter.map₂_right theorem

[NeBot f] : map₂ (fun _ y => y) f g = g

Full source

@[simp]
theorem map₂_right [NeBot f] : map₂ (fun _ y => y) f g = g := by rw [map₂_swap, map₂_left]

Right Projection of Binary Image Filter Equals Second Filter

Informal description

For any filter $g$ on a type $\beta$ and any non-trivial filter $f$ on a type $\alpha$, the binary image filter of the projection function $(\_, y) \mapsto y$ applied to $f$ and $g$ equals $g$.

Filter.map_map₂ theorem

(m : α → β → γ) (n : γ → δ) : (map₂ m f g).map n = map₂ (fun a b => n (m a b)) f g

Full source

theorem map_map₂ (m : α → β → γ) (n : γ → δ) :
    (map₂ m f g).map n = map₂ (fun a b => n (m a b)) f g := by
  rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]; rfl

Composition of Binary Image Filter with Unary Map: $\text{map}_n \circ \text{map}_2 \, m = \text{map}_2 \, (n \circ m)$

Informal description

For any binary function $m \colon \alpha \to \beta \to \gamma$, any function $n \colon \gamma \to \delta$, and filters $f$ on $\alpha$ and $g$ on $\beta$, the following equality holds: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, (n \circ m) \, f \, g \] where $\text{map}_n$ denotes the image filter under $n$ and $\text{map}_2$ denotes the binary image filter operation.

Filter.map₂_map_left theorem

(m : γ → β → δ) (n : α → γ) : map₂ m (f.map n) g = map₂ (fun a b => m (n a) b) f g

Full source

theorem map₂_map_left (m : γ → β → δ) (n : α → γ) :
    map₂ m (f.map n) g = map₂ (fun a b => m (n a) b) f g := by
  rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id]; rfl

Left Composition of Binary Image Filter with Unary Map: $\text{map}_2 \, m \circ \text{map}_n = \text{map}_2 \, (m \circ n)$

Informal description

For any function $m \colon \gamma \to \beta \to \delta$, any function $n \colon \alpha \to \gamma$, and filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, (\text{map}_n f) \, g$ is equal to the binary image filter $\text{map}_2 \, (m \circ n) \, f \, g$. In symbols: \[ \text{map}_2 \, m \, (\text{map}_n f) \, g = \text{map}_2 \, (m \circ n) \, f \, g \]

Filter.map₂_map_right theorem

(m : α → γ → δ) (n : β → γ) : map₂ m f (g.map n) = map₂ (fun a b => m a (n b)) f g

Full source

theorem map₂_map_right (m : α → γ → δ) (n : β → γ) :
    map₂ m f (g.map n) = map₂ (fun a b => m a (n b)) f g := by
  rw [map₂_swap, map₂_map_left, map₂_swap]

Right Composition of Binary Image Filter with Unary Map: $\text{map}_2 \, m \circ \text{map}_n = \text{map}_2 \, (m \circ n)$

Informal description

For any binary function $m \colon \alpha \to \gamma \to \delta$, any function $n \colon \beta \to \gamma$, and filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filter $\text{map}_2 \, m \, f \, (\text{map}_n g)$ is equal to the binary image filter $\text{map}_2 \, (\lambda a b, m a (n b)) \, f \, g$. In symbols: \[ \text{map}_2 \, m \, f \, (\text{map}_n g) = \text{map}_2 \, (\lambda a b, m a (n b)) \, f \, g \]

Filter.map₂_curry theorem

(m : α × β → γ) (f : Filter α) (g : Filter β) : map₂ m.curry f g = (f ×ˢ g).map m

Full source

@[simp]
theorem map₂_curry (m : α × β → γ) (f : Filter α) (g : Filter β) :
    map₂ m.curry f g = (f ×ˢ g).map m :=
  (map_prod_eq_map₂' _ _ _).symm

Equality of Binary Image Filter via Currying and Product Image Filter

Informal description

For any function $m \colon \alpha \times \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filter of the curried function $m.curry$ applied to $f$ and $g$ is equal to the image filter of $m$ under the product filter $f \times^s g$. That is, \[ \text{map}_2 (m.curry) \, f \, g = \text{map}(m)(f \times^s g). \]

Filter.map_uncurry_prod theorem

(m : α → β → γ) (f : Filter α) (g : Filter β) : (f ×ˢ g).map (uncurry m) = map₂ m f g

Full source

@[simp]
theorem map_uncurry_prod (m : α → β → γ) (f : Filter α) (g : Filter β) :
    (f ×ˢ g).map (uncurry m) = map₂ m f g :=
  (map₂_curry (uncurry m) f g).symm

Equality of Product Image Filter and Binary Image Filter via Uncurrying

Informal description

For any binary function $m \colon \alpha \times \beta \to \gamma$ and filters $f$ on $\alpha$ and $g$ on $\beta$, the image filter of the uncurried function $\text{uncurry}(m)$ under the product filter $f \times^s g$ is equal to the binary image filter of $m$ applied to $f$ and $g$. That is, \[ \text{map}(\text{uncurry}(m))(f \times^s g) = \text{map}_2(m) f g. \]

Filter.map₂_assoc theorem

 {m : δ → γ → ε} {n : α → β → δ} {m' : α → ε' → ε} {n' : β → γ → ε'} {h : Filter γ}
  (h_assoc : ∀ a b c, m (n a b) c = m' a (n' b c)) : map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)

Full source

theorem map₂_assoc {m : δ → γ → ε} {n : α → β → δ} {m' : α → ε' → ε} {n' : β → γ → ε'}
    {h : Filter γ} (h_assoc : ∀ a b c, m (n a b) c = m' a (n' b c)) :
    map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h) := by
  rw [← map_prod_eq_map₂ n, ← map_prod_eq_map₂ n', map₂_map_left, map₂_map_right,
    ← map_prod_eq_map₂, ← map_prod_eq_map₂, ← prod_assoc, map_map]
  simp only [h_assoc, Function.comp_def, Equiv.prodAssoc_apply]

Associativity of Binary Image Filters: $\text{map}_2 \, m \circ (\text{map}_2 \, n) = \text{map}_2 \, m' \circ (\text{map}_2 \, n')$ under associativity condition

Informal description

Let $m \colon \delta \to \gamma \to \varepsilon$, $n \colon \alpha \to \beta \to \delta$, $m' \colon \alpha \to \varepsilon' \to \varepsilon$, and $n' \colon \beta \to \gamma \to \varepsilon'$ be functions, and let $f$, $g$, and $h$ be filters on $\alpha$, $\beta$, and $\gamma$ respectively. Suppose that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the associativity condition \[ m(n(a, b), c) = m'(a, n'(b, c)) \] holds. Then the binary image filters satisfy: \[ \text{map}_2 \, m \, (\text{map}_2 \, n \, f \, g) \, h = \text{map}_2 \, m' \, f \, (\text{map}_2 \, n' \, g \, h). \]

Filter.map₂_comm theorem

{n : β → α → γ} (h_comm : ∀ a b, m a b = n b a) : map₂ m f g = map₂ n g f

Full source

theorem map₂_comm {n : β → α → γ} (h_comm : ∀ a b, m a b = n b a) : map₂ m f g = map₂ n g f :=
  (map₂_swap _ _ _).trans <| by simp_rw [h_comm]

Commutativity of Binary Image Filter: $\text{map}_2 \, m \, f \, g = \text{map}_2 \, n \, g \, f$ when $m$ and $n$ are swapped

Informal description

Let $m : \alpha \to \beta \to \gamma$ and $n : \beta \to \alpha \to \gamma$ be binary functions such that $m(a, b) = n(b, a)$ for all $a \in \alpha$ and $b \in \beta$. Then for any filters $f$ on $\alpha$ and $g$ on $\beta$, the binary image filters satisfy $\text{map}_2 \, m \, f \, g = \text{map}_2 \, n \, g \, f$.

Filter.map₂_left_comm theorem

 {m : α → δ → ε} {n : β → γ → δ} {m' : α → γ → δ'} {n' : β → δ' → ε}
  (h_left_comm : ∀ a b c, m a (n b c) = n' b (m' a c)) : map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Full source

theorem map₂_left_comm {m : α → δ → ε} {n : β → γ → δ} {m' : α → γ → δ'} {n' : β → δ' → ε}
    (h_left_comm : ∀ a b c, m a (n b c) = n' b (m' a c)) :
    map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h) := by
  rw [map₂_swap m', map₂_swap m]
  exact map₂_assoc fun _ _ _ => h_left_comm _ _ _

Left-commutativity of binary image filters: $\text{map}_2 \, m \circ (f \times \text{map}_2 \, n) = \text{map}_2 \, n' \circ (g \times \text{map}_2 \, m')$ under left-commutativity condition

Informal description

Let $m \colon \alpha \to \delta \to \varepsilon$, $n \colon \beta \to \gamma \to \delta$, $m' \colon \alpha \to \gamma \to \delta'$, and $n' \colon \beta \to \delta' \to \varepsilon$ be functions, and let $f$, $g$, and $h$ be filters on $\alpha$, $\beta$, and $\gamma$ respectively. Suppose that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the left-commutativity condition \[ m(a, n(b, c)) = n'(b, m'(a, c)) \] holds. Then the binary image filters satisfy: \[ \text{map}_2 \, m \, f \, (\text{map}_2 \, n \, g \, h) = \text{map}_2 \, n' \, g \, (\text{map}_2 \, m' \, f \, h). \]

Filter.map₂_right_comm theorem

 {m : δ → γ → ε} {n : α → β → δ} {m' : α → γ → δ'} {n' : δ' → β → ε}
  (h_right_comm : ∀ a b c, m (n a b) c = n' (m' a c) b) : map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g

Full source

theorem map₂_right_comm {m : δ → γ → ε} {n : α → β → δ} {m' : α → γ → δ'} {n' : δ' → β → ε}
    (h_right_comm : ∀ a b c, m (n a b) c = n' (m' a c) b) :
    map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g := by
  rw [map₂_swap n, map₂_swap n']
  exact map₂_assoc fun _ _ _ => h_right_comm _ _ _

Right Commutativity of Binary Image Filters under Right-Commutativity Condition

Informal description

Let $m \colon \delta \to \gamma \to \varepsilon$, $n \colon \alpha \to \beta \to \delta$, $m' \colon \alpha \to \gamma \to \delta'$, and $n' \colon \delta' \to \beta \to \varepsilon$ be functions, and let $f$, $g$, and $h$ be filters on $\alpha$, $\beta$, and $\gamma$ respectively. Suppose that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the right-commutativity condition \[ m(n(a, b), c) = n'(m'(a, c), b) \] holds. Then the binary image filters satisfy: \[ \text{map}_2 \, m \, (\text{map}_2 \, n \, f \, g) \, h = \text{map}_2 \, n' \, (\text{map}_2 \, m' \, f \, h) \, g. \]

Filter.map_map₂_distrib theorem

 {n : γ → δ} {m' : α' → β' → δ} {n₁ : α → α'} {n₂ : β → β'} (h_distrib : ∀ a b, n (m a b) = m' (n₁ a) (n₂ b)) :
  (map₂ m f g).map n = map₂ m' (f.map n₁) (g.map n₂)

Full source

theorem map_map₂_distrib {n : γ → δ} {m' : α' → β' → δ} {n₁ : α → α'} {n₂ : β → β'}
    (h_distrib : ∀ a b, n (m a b) = m' (n₁ a) (n₂ b)) :
    (map₂ m f g).map n = map₂ m' (f.map n₁) (g.map n₂) := by
  simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]

Distributive Property of Binary Image Filter Composition: $\text{map}_n \circ \text{map}_2 \, m = \text{map}_2 \, m' \circ (\text{map}_{n_1} \times \text{map}_{n_2})$

Informal description

For any functions $n \colon \gamma \to \delta$, $m' \colon \alpha' \to \beta' \to \delta$, $n_1 \colon \alpha \to \alpha'$, and $n_2 \colon \beta \to \beta'$ satisfying the distributive property: \[ \forall a \in \alpha, b \in \beta, \quad n(m(a, b)) = m'(n_1(a), n_2(b)), \] the following equality of filters holds: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, m' \, (\text{map}_{n_1} f) \, (\text{map}_{n_2} g). \]

Filter.map_map₂_distrib_left theorem

 {n : γ → δ} {m' : α' → β → δ} {n' : α → α'} (h_distrib : ∀ a b, n (m a b) = m' (n' a) b) :
  (map₂ m f g).map n = map₂ m' (f.map n') g

Full source

/-- Symmetric statement to `Filter.map₂_map_left_comm`. -/
theorem map_map₂_distrib_left {n : γ → δ} {m' : α' → β → δ} {n' : α → α'}
    (h_distrib : ∀ a b, n (m a b) = m' (n' a) b) : (map₂ m f g).map n = map₂ m' (f.map n') g :=
  map_map₂_distrib h_distrib

Left Distributive Property of Binary Image Filter Composition

Informal description

For any functions $n \colon \gamma \to \delta$, $m' \colon \alpha' \to \beta \to \delta$, and $n' \colon \alpha \to \alpha'$ satisfying the distributive property: \[ \forall a \in \alpha, b \in \beta, \quad n(m(a, b)) = m'(n'(a), b), \] the following equality of filters holds: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, m' \, (\text{map}_{n'} f) \, g. \]

Filter.map_map₂_distrib_right theorem

 {n : γ → δ} {m' : α → β' → δ} {n' : β → β'} (h_distrib : ∀ a b, n (m a b) = m' a (n' b)) :
  (map₂ m f g).map n = map₂ m' f (g.map n')

Full source

/-- Symmetric statement to `Filter.map_map₂_right_comm`. -/
theorem map_map₂_distrib_right {n : γ → δ} {m' : α → β' → δ} {n' : β → β'}
    (h_distrib : ∀ a b, n (m a b) = m' a (n' b)) : (map₂ m f g).map n = map₂ m' f (g.map n') :=
  map_map₂_distrib h_distrib

Right Distributive Property of Binary Image Filter Composition

Informal description

For any functions $n \colon \gamma \to \delta$, $m' \colon \alpha \to \beta' \to \delta$, and $n' \colon \beta \to \beta'$ satisfying the distributive property: \[ \forall a \in \alpha, b \in \beta, \quad n(m(a, b)) = m'(a, n'(b)), \] the following equality of filters holds: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, m' \, f \, (\text{map}_{n'} g). \]

Filter.map_map₂_right_comm theorem

 {m : α → β' → γ} {n : β → β'} {m' : α → β → δ} {n' : δ → γ} (h_right_comm : ∀ a b, m a (n b) = n' (m' a b)) :
  map₂ m f (g.map n) = (map₂ m' f g).map n'

Full source

/-- Symmetric statement to `Filter.map_map₂_distrib_right`. -/
theorem map_map₂_right_comm {m : α → β' → γ} {n : β → β'} {m' : α → β → δ} {n' : δ → γ}
    (h_right_comm : ∀ a b, m a (n b) = n' (m' a b)) : map₂ m f (g.map n) = (map₂ m' f g).map n' :=
  (map_map₂_distrib_right fun a b => (h_right_comm a b).symm).symm

Right Commutative Property of Binary Image Filter Composition

Informal description

For any functions $m \colon \alpha \to \beta' \to \gamma$, $n \colon \beta \to \beta'$, $m' \colon \alpha \to \beta \to \delta$, and $n' \colon \delta \to \gamma$ satisfying the right commutative property: \[ \forall a \in \alpha, b \in \beta, \quad m(a, n(b)) = n'(m'(a, b)), \] the following equality of filters holds: \[ \text{map}_2 \, m \, f \, (\text{map}_n \, g) = \text{map}_{n'} (\text{map}_2 \, m' \, f \, g). \]

Filter.map₂_distrib_le_left theorem

 {m : α → δ → ε} {n : β → γ → δ} {m₁ : α → β → β'} {m₂ : α → γ → γ'} {n' : β' → γ' → ε}
  (h_distrib : ∀ a b c, m a (n b c) = n' (m₁ a b) (m₂ a c)) :
  map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h)

Full source

/-- The other direction does not hold because of the `f-f` cross terms on the RHS. -/
theorem map₂_distrib_le_left {m : α → δ → ε} {n : β → γ → δ} {m₁ : α → β → β'} {m₂ : α → γ → γ'}
    {n' : β' → γ' → ε} (h_distrib : ∀ a b c, m a (n b c) = n' (m₁ a b) (m₂ a c)) :
    map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h) := by
  rintro s ⟨t₁, ⟨u₁, hu₁, v, hv, ht₁⟩, t₂, ⟨u₂, hu₂, w, hw, ht₂⟩, hs⟩
  refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩
  refine (image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)
  · exact (image2_subset_right inter_subset_left).trans ht₁
  · exact (image2_subset_right inter_subset_right).trans ht₂

Left Distributivity Inequality for Binary Filter Mapping

Informal description

Let $m : \alpha \to \delta \to \varepsilon$, $n : \beta \to \gamma \to \delta$, $m_1 : \alpha \to \beta \to \beta'$, $m_2 : \alpha \to \gamma \to \gamma'$, and $n' : \beta' \to \gamma' \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the following distributive property holds: \[ m(a, n(b, c)) = n'(m_1(a, b), m_2(a, c)). \] Then, for any filters $f$ on $\alpha$, $g$ on $\beta$, and $h$ on $\gamma$, we have the inequality: \[ \text{map}_2(m, f, \text{map}_2(n, g, h)) \leq \text{map}_2(n', \text{map}_2(m_1, f, g), \text{map}_2(m_2, f, h)). \]

Filter.map₂_distrib_le_right theorem

 {m : δ → γ → ε} {n : α → β → δ} {m₁ : α → γ → α'} {m₂ : β → γ → β'} {n' : α' → β' → ε}
  (h_distrib : ∀ a b c, m (n a b) c = n' (m₁ a c) (m₂ b c)) :
  map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h)

Full source

/-- The other direction does not hold because of the `h`-`h` cross terms on the RHS. -/
theorem map₂_distrib_le_right {m : δ → γ → ε} {n : α → β → δ} {m₁ : α → γ → α'} {m₂ : β → γ → β'}
    {n' : α' → β' → ε} (h_distrib : ∀ a b c, m (n a b) c = n' (m₁ a c) (m₂ b c)) :
    map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h) := by
  rintro s ⟨t₁, ⟨u, hu, w₁, hw₁, ht₁⟩, t₂, ⟨v, hv, w₂, hw₂, ht₂⟩, hs⟩
  refine ⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩
  refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)
  · exact (image2_subset_left inter_subset_left).trans ht₁
  · exact (image2_subset_left inter_subset_right).trans ht₂

Right Distributivity Inequality for Binary Filter Mapping

Informal description

Let $m : \delta \to \gamma \to \varepsilon$, $n : \alpha \to \beta \to \delta$, $m_1 : \alpha \to \gamma \to \alpha'$, $m_2 : \beta \to \gamma \to \beta'$, and $n' : \alpha' \to \beta' \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the following distributive property holds: \[ m(n(a, b), c) = n'(m_1(a, c), m_2(b, c)). \] Then, for any filters $f$ on $\alpha$, $g$ on $\beta$, and $h$ on $\gamma$, we have the inequality: \[ \text{map}_2(m, \text{map}_2(n, f, g), h) \leq \text{map}_2(n', \text{map}_2(m_1, f, h), \text{map}_2(m_2, g, h)). \]

Filter.map_map₂_antidistrib theorem

 {n : γ → δ} {m' : β' → α' → δ} {n₁ : β → β'} {n₂ : α → α'} (h_antidistrib : ∀ a b, n (m a b) = m' (n₁ b) (n₂ a)) :
  (map₂ m f g).map n = map₂ m' (g.map n₁) (f.map n₂)

Full source

theorem map_map₂_antidistrib {n : γ → δ} {m' : β' → α' → δ} {n₁ : β → β'} {n₂ : α → α'}
    (h_antidistrib : ∀ a b, n (m a b) = m' (n₁ b) (n₂ a)) :
    (map₂ m f g).map n = map₂ m' (g.map n₁) (f.map n₂) := by
  rw [map₂_swap m]
  exact map_map₂_distrib fun _ _ => h_antidistrib _ _

Antidistributive Property of Binary Image Filter Composition: $\text{map}_n \circ \text{map}_2 \, m = \text{map}_2 \, m' \circ (\text{map}_{n_1} \times \text{map}_{n_2})^{\text{op}}$

Informal description

For any functions $n \colon \gamma \to \delta$, $m' \colon \beta' \to \alpha' \to \delta$, $n_1 \colon \beta \to \beta'$, and $n_2 \colon \alpha \to \alpha'$ satisfying the antidistributive property: \[ \forall a \in \alpha, b \in \beta, \quad n(m(a, b)) = m'(n_1(b), n_2(a)), \] the following equality of filters holds: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, m' \, (\text{map}_{n_1} g) \, (\text{map}_{n_2} f). \]

Filter.map_map₂_antidistrib_left theorem

 {n : γ → δ} {m' : β' → α → δ} {n' : β → β'} (h_antidistrib : ∀ a b, n (m a b) = m' (n' b) a) :
  (map₂ m f g).map n = map₂ m' (g.map n') f

Full source

/-- Symmetric statement to `Filter.map₂_map_left_anticomm`. -/
theorem map_map₂_antidistrib_left {n : γ → δ} {m' : β' → α → δ} {n' : β → β'}
    (h_antidistrib : ∀ a b, n (m a b) = m' (n' b) a) : (map₂ m f g).map n = map₂ m' (g.map n') f :=
  map_map₂_antidistrib h_antidistrib

Left Antidistributivity of Filter Mapping Composition: $\text{map}_n \circ \text{map}_2 \, m = \text{map}_2 \, m' \circ (\text{map}_{n'} \times \text{id})$

Informal description

Let $n \colon \gamma \to \delta$, $m' \colon \beta' \to \alpha \to \delta$, and $n' \colon \beta \to \beta'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following antidistributive property holds: \[ n(m(a, b)) = m'(n'(b), a). \] Then for any filters $f$ on $\alpha$ and $g$ on $\beta$, we have the equality of filters: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, m' \, (\text{map}_{n'} g) \, f. \]

Filter.map_map₂_antidistrib_right theorem

 {n : γ → δ} {m' : β → α' → δ} {n' : α → α'} (h_antidistrib : ∀ a b, n (m a b) = m' b (n' a)) :
  (map₂ m f g).map n = map₂ m' g (f.map n')

Full source

/-- Symmetric statement to `Filter.map_map₂_right_anticomm`. -/
theorem map_map₂_antidistrib_right {n : γ → δ} {m' : β → α' → δ} {n' : α → α'}
    (h_antidistrib : ∀ a b, n (m a b) = m' b (n' a)) : (map₂ m f g).map n = map₂ m' g (f.map n') :=
  map_map₂_antidistrib h_antidistrib

Right Antidistributive Property of Binary Image Filter Composition: $\text{map}_n \circ \text{map}_2 \, m = \text{map}_2 \, m' \circ (\text{id} \times \text{map}_{n'})$

Informal description

For any functions $n \colon \gamma \to \delta$, $m' \colon \beta \to \alpha' \to \delta$, and $n' \colon \alpha \to \alpha'$ satisfying the right antidistributive property: \[ \forall a \in \alpha, b \in \beta, \quad n(m(a, b)) = m'(b, n'(a)), \] the following equality of filters holds: \[ \text{map}_n (\text{map}_2 \, m \, f \, g) = \text{map}_2 \, m' \, g \, (\text{map}_{n'} f). \]

Filter.map₂_map_left_anticomm theorem

 {m : α' → β → γ} {n : α → α'} {m' : β → α → δ} {n' : δ → γ} (h_left_anticomm : ∀ a b, m (n a) b = n' (m' b a)) :
  map₂ m (f.map n) g = (map₂ m' g f).map n'

Full source

/-- Symmetric statement to `Filter.map_map₂_antidistrib_left`. -/
theorem map₂_map_left_anticomm {m : α' → β → γ} {n : α → α'} {m' : β → α → δ} {n' : δ → γ}
    (h_left_anticomm : ∀ a b, m (n a) b = n' (m' b a)) :
    map₂ m (f.map n) g = (map₂ m' g f).map n' :=
  (map_map₂_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm

Left Anticommutative Property of Binary Image Filter Composition: $\text{map}_2 \, m \circ (\text{map}_n \times \text{id}) = \text{map}_{n'} \circ \text{map}_2 \, m' \circ \text{swap}$

Informal description

Let $m \colon \alpha' \to \beta \to \gamma$, $n \colon \alpha \to \alpha'$, $m' \colon \beta \to \alpha \to \delta$, and $n' \colon \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following left anticommutative property holds: \[ m(n(a), b) = n'(m'(b, a)). \] Then for any filters $f$ on $\alpha$ and $g$ on $\beta$, we have the equality of filters: \[ \text{map}_2 \, m \, (\text{map}_n f) \, g = \text{map}_{n'} (\text{map}_2 \, m' \, g \, f). \]

Filter.map_map₂_right_anticomm theorem

 {m : α → β' → γ} {n : β → β'} {m' : β → α → δ} {n' : δ → γ} (h_right_anticomm : ∀ a b, m a (n b) = n' (m' b a)) :
  map₂ m f (g.map n) = (map₂ m' g f).map n'

Full source

/-- Symmetric statement to `Filter.map_map₂_antidistrib_right`. -/
theorem map_map₂_right_anticomm {m : α → β' → γ} {n : β → β'} {m' : β → α → δ} {n' : δ → γ}
    (h_right_anticomm : ∀ a b, m a (n b) = n' (m' b a)) :
    map₂ m f (g.map n) = (map₂ m' g f).map n' :=
  (map_map₂_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm

Right Anticommutative Property of Binary Image Filter Composition: $\text{map}_2 \, m \circ (\text{id} \times \text{map}_n) = \text{map}_{n'} \circ \text{map}_2 \, m' \circ \text{swap}$

Informal description

For any functions $m \colon \alpha \to \beta' \to \gamma$, $n \colon \beta \to \beta'$, $m' \colon \beta \to \alpha \to \delta$, and $n' \colon \delta \to \gamma$ satisfying the right anticommutativity condition: \[ \forall a \in \alpha, b \in \beta, \quad m(a, n(b)) = n'(m'(b, a)), \] the following equality of filters holds: \[ \text{map}_2 \, m \, f \, (\text{map}_n \, g) = \text{map}_{n'} (\text{map}_2 \, m' \, g \, f). \]

Filter.map₂_left_identity theorem

{f : α → β → β} {a : α} (h : ∀ b, f a b = b) (l : Filter β) : map₂ f (pure a) l = l

Full source

/-- If `a` is a left identity for `f : α → β → β`, then `pure a` is a left identity for
`Filter.map₂ f`. -/
theorem map₂_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (l : Filter β) :
    map₂ f (pure a) l = l := by rw [map₂_pure_left, show f a = id from funext h, map_id]

Left Identity Property for Binary Image Filter

Informal description

Let $f \colon \alpha \to \beta \to \beta$ be a binary function and $a \in \alpha$ be a left identity for $f$, meaning that $f(a, b) = b$ for all $b \in \beta$. Then for any filter $l$ on $\beta$, the binary image filter $\text{map}_2 \, f \, (\text{pure } a) \, l$ is equal to $l$.

Filter.map₂_right_identity theorem

{f : α → β → α} {b : β} (h : ∀ a, f a b = a) (l : Filter α) : map₂ f l (pure b) = l

Full source

/-- If `b` is a right identity for `f : α → β → α`, then `pure b` is a right identity for
`Filter.map₂ f`. -/
theorem map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (l : Filter α) :
    map₂ f l (pure b) = l := by rw [map₂_pure_right, funext h, map_id']

Right Identity Property for Binary Image Filter

Informal description

Let $f : \alpha \to \beta \to \alpha$ be a binary function and $b \in \beta$ be a right identity for $f$, meaning that $f(a, b) = a$ for all $a \in \alpha$. Then for any filter $l$ on $\alpha$, the binary image filter $\text{map}_2 \, f \, l \, (\text{pure } b)$ is equal to $l$.

Mathlib.Order.Filter.NAry

Main declarations

Notes