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
and to data.finset.n_ary
.
Please keep them in sync.
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 := _}
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 := _}
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
.
Symmetric of filter.map₂_map_left_comm
.
Symmetric of filter.map_map₂_right_comm
.
Symmetric of filter.map_map₂_distrib_left
.
Symmetric of filter.map_map₂_distrib_right
.
The other direction does not hold because of the f
-f
cross terms on the RHS.
The other direction does not hold because of the h
-h
cross terms on the RHS.
Symmetric of filter.map₂_map_left_anticomm
.
Symmetric of filter.map_map₂_right_anticomm
.
Symmetric of filter.map_map₂_antidistrib_left
.
Symmetric of filter.map_map₂_antidistrib_right
.