Filter.map₂_bot_left
theorem Filter.map₂_bot_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {g : Filter β}, Filter.map₂ m ⊥ g = ⊥
The theorem `Filter.map₂_bot_left` states that for any types `α`, `β`, and `γ`, and any binary function `m : α → β → γ` and filter `g : Filter β`, mapping `m` over the least (bottom) filter and `g` results in the least filter. In other words, the image of the least filter and any other filter under a binary function is always the least filter.
More concisely: Given any types α, β, and γ, binary function m : α → β → γ, and filter g on β, the application of the function m to the least filter on α and filter g results in the least filter on the image of g under m.
|
Filter.image2_mem_map₂
theorem Filter.image2_mem_map₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} {s : Set α}
{t : Set β}, s ∈ f → t ∈ g → Set.image2 m s t ∈ Filter.map₂ m f g
This theorem states that for any types `α`, `β`, and `γ`, any binary function `m` mapping from `α` and `β` to `γ`, any filters `f` on `α` and `g` on `β`, and any sets `s` of `α` and `t` of `β`, if `s` is in the filter `f` and `t` is in the filter `g`, then the image of the function `m` over sets `s` and `t`, denoted `Set.image2 m s t`, is in the filter `Filter.map₂ m f g`, where `Filter.map₂` is the mapping of the binary function `m` from filters `f` and `g` to a filter on `γ`. This essentially asserts that if `s` and `t` are sets filtered by `f` and `g` respectively, then the set of all values generated by applying `m` to every pair of elements from `s` and `t` is also filtered under the mapping of `m` over `f` and `g`.
More concisely: Given types `α`, `β`, `γ`, a binary function `m` from `α` and `β` to `γ`, filters `f` on `α` and `g` on `β`, and sets `s` of `α` and `t` of `β` such that `s ∈ f` and `t ∈ g`, then `Set.image2 m s t ∈ Filter.map₂ m f g`.
|
Filter.map₂_swap
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
The `Filter.map₂_swap` theorem states that for any types `α`, `β`, and `γ` and any binary function `m : α → β → γ` and filters `f : Filter α` and `g : Filter β`, mapping with `m` over `f` and `g` is the same as swapping the arguments of `m` and mapping over `g` and `f`. In other words, the order of filters and the corresponding swap in the function's parameters do not affect the output when using the `Filter.map₂` function. This is reminiscent of the mathematical concept that the image of a function remains the same when the order of its arguments is interchanged.
More concisely: For any types `α`, `β`, `γ`, filters `f : Filter α` and `g : Filter β`, and binary function `m : α → β → γ`, `Filter.map₂ m f g` is equal to `Filter.map₂ (λ x y => m y x) g f`.
|
Filter.map₂_map_left_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' : δ → γ},
(∀ (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)
The theorem `Filter.map₂_map_left_anticomm` states that, for any types `α`, `α'`, `β`, `γ`, and `δ`, any filters `f` and `g` on `α` and `β` respectively, any binary functions `m : α' → β → γ` and `m' : β → α → δ`, and any unary functions `n : α → α'` and `n' : δ → γ`, if for all `a` in `α` and `b` in `β`, the function `m` applied to `n a` and `b` equals the function `n'` applied to `m' b a`, then mapping the binary function `m` over the filter `f` mapped by `n` and the filter `g` is equal to mapping `n'` over the map of the binary function `m'` over `g` and `f`. In other words, the theorem states a certain kind of commutativity of the `map` and `map₂` operations on filters under these conditions.
More concisely: If for all `a` in `α` and `b` in `β`, `m (n a) b = n' (m' b a)`, then `(map₂ m (map_filter f n) g) = (map (n') (map₂ m' g (map_filter f id)))`.
|
Filter.map₂_left_identity
theorem Filter.map₂_left_identity :
∀ {α : Type u_1} {β : Type u_3} {f : α → β → β} {a : α},
(∀ (b : β), f a b = b) → ∀ (l : Filter β), Filter.map₂ f (pure a) l = l
The theorem `Filter.map₂_left_identity` states that for any types `α` and `β`, any binary function `f : α → β → β`, and any element `a : α`, if `a` serves as a left identity for `f`, meaning that applying `f` to `a` and any element of `β` always yields that element of `β` back (`∀ (b : β), f a b = b`), then the `Filter.map₂` of `f` applied to the `pure` filter of `a` and any filter `l` of type `β` is equal to `l`. In other words, the `pure` filter of `a` acts as a left identity for `Filter.map₂ f`.
More concisely: If `f : α → β → β` is a binary function with left identity `a : α` such that `f a b = b` for all `b : β`, then `Filter.map₂ f (Filter.pure a) = id` (identity filter) on type `β`.
|
Filter.map_map₂_distrib_right
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' : β → β'},
(∀ (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)
The theorem `Filter.map_map₂_distrib_right` states that for all types `α`, `β`, `β'`, `γ`, and `δ`, for any filters `f` of type `α` and `g` of type `β`, for any binary function `m : α → β → γ`, any function `n : γ → δ` and `n' : β → β'` and a binary function `m' : α → β' → δ`, if for every `α` and `β`, the function `n` applied to the result of `m` applied to `α` and `β` equals the result of `m'` applied to `α` and `n'` applied to `β`, then the filter obtained by mapping `n` over the filter obtained by applying `m` to filters `f` and `g` is equal to the filter obtained by applying `m'` to filter `f` and the filter obtained by mapping `n'` over filter `g`. In other words, this theorem is about the distributivity of mapping operations over filters in a particular way.
More concisely: If for all `α`, `β`, `β'`, `γ`, and `δ`, and functions `m : α → β → γ`, `n : γ → δ`, `m' : α → β' → δ`, `n' : β → β'`, the equality `n (m x y) = m' x (n' y)` holds for all `x : α` and `y : β`, then `Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' f (Filter.map n' g)`, where `f` and `g` are filters on types `α` and `β`, respectively.
|
Filter.map₂_mono
theorem Filter.map₂_mono :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β},
f₁ ≤ f₂ → g₁ ≤ g₂ → Filter.map₂ m f₁ g₁ ≤ Filter.map₂ m f₂ g₂
The theorem `Filter.map₂_mono` states that for all types `α`, `β`, and `γ`, for all binary functions `m : α → β → γ`, for all filters `f₁`, `f₂` on `α` and `g₁`, `g₂` on `β`, if `f₁` is a subfilter of `f₂` and `g₁` is a subfilter of `g₂` (meaning every set in `f₁` is also in `f₂` and every set in `g₁` is also in `g₂`), then the image of `m` under the filters `f₁` and `g₁` is a subfilter of the image of `m` under the filters `f₂` and `g₂`. In mathematical terms, this can be expressed as if $f_1 \subseteq f_2$ and $g_1 \subseteq g_2$ then $m(f_1, g_1) \subseteq m(f_2, g_2)$ where $m$ is the map function, $f_1, f_2$ are filters on $\alpha$ and $g_1, g_2$ are filters on $\beta$.
More concisely: If filters $f\_1 \subseteq f\_2$ on type $\alpha$ and filters $g\_1 \subseteq g\_2$ on type $\beta$, then the image of the binary function $m : \alpha \times \beta \rightarrow \gamma$ under filters $f\_1 \times g\_1$ is a subfilter of the image under filters $f\_2 \times g\_2$.
|
Mathlib.Order.Filter.NAry._auxLemma.6
theorem Mathlib.Order.Filter.NAry._auxLemma.6 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : Filter α) (g : Filter β),
Filter.map₂ m f g = Filter.map (fun p => m p.1 p.2) (f ×ˢ g)
This theorem states that, for any types `α`, `β`, and `γ`, and for any binary function `m : α → β → γ` and filters `f : Filter α` and `g : Filter β`, the image of the binary function `m` as a function from filters `f` and `g` to `Filter γ` (denoted as `Filter.map₂ m f g`) is the same as the image of the function that takes a pair `p` and maps it to the result of applying `m` to the elements of `p` (i.e., `m p.1 p.2`), under the filter formed by the product of `f` and `g` (denoted as `Filter.map (fun p => m p.1 p.2) (f ×ˢ g)`). This is a statement about the equivalence of two different ways to construct the image of a function under a filter.
More concisely: For any functions `m : α -> β -> γ`, `f : Filter α`, and `g : Filter β`, `Filter.map₂ m f g = Filter.map (fun p => m p.1 p.2) (f ×ˢ g)` (where `p` is a pair from `α x β`).
|
Filter.map₂_pure
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)
This theorem, `Filter.map₂_pure`, states that for any binary function `m` of type `α → β → γ`, and any two elements `a` of type `α` and `b` of type `β`, the image of the function `m` under the filters `pure a` and `pure b` (which are the filters containing only the elements `a` and `b` respectively) is equal to the filter containing only the element `m a b`. In mathematical terms, if we consider the function `m` as a mapping from the Cartesian product `α × β` to `γ`, then applying this function to the pairs `(a, b)` where `a` and `b` are specific elements of `α` and `β` respectively, produces the same result as applying the function `m` to `a` and `b` directly and taking the filter containing only this result.
More concisely: For any binary function `m` and elements `a` and `b`, `Filter.map₂ m (pure a) (pure b) = pure (m a b)`.
|
Filter.map₂_map_left_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' : δ → γ},
(∀ (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)
This theorem, named `Filter.map₂_map_left_comm`, establishes the commutation relation between two operations: the `map` operation on filters and the `map₂` operation, which is the image of a binary function on filters. The theorem states that for all types `α`, `α'`, `β`, `γ`, `δ`, and for all filters `f` and `g` of types `α` and `β` respectively, and for all functions `m : α' → β → γ`, `n : α → α'`, `m' : α → β → δ`, `n' : δ → γ`, if the function `m` composed with `n` is equal to the function `n'` composed with `m'` for all elements of the domains, then the image of the binary function `m` on the image of the function `n` on the filter `f` and the filter `g` is equal to the image of the function `n'` on the image of the binary function `m'` on the filter `f` and the filter `g`. This theorem can be used to interchange the operations of `map` and `map₂` under certain conditions.
More concisely: If `m (n x) = n' (m' x)` for all `x`, then `(map₂ m n) (f ∧ g) = (map (n') (map m) (f ∧ g))`.
|
Filter.map_map₂
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
The theorem `Filter.map_map₂` states that for all types `α`, `β`, `γ`, and `δ`, and for any filters `f` on `α` and `g` on `β`, if we have a binary function `m` from `α` and `β` to `γ`, and a function `n` from `γ` to `δ`, then mapping `n` over the filter obtained by applying the binary map `map₂` of `m` on `f` and `g` is equal to applying the binary map `map₂` of the function `(a, b) ↦ n (m a b)` directly on `f` and `g`. Essentially, this theorem shows that the operation of filter mapping is compatible with composition of functions.
More concisely: For all types `α`, `β`, `γ`, `δ`, filters `f` on `α` and `g` on `β`, and functions `m : α → β → γ` and `n : γ → δ`, `map₂ n (map₂ m (f : Filter α) (g : Filter β)) = map₂ (λ a b, n (m a b)) (f) (g)`.
|
Filter.map₂_assoc
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 γ},
(∀ (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)
This theorem is about the association of binary function mappings over filters. It states that for all types `α`, `β`, `γ`, `δ`, `ε`, `ε'`, for filters `f` over type `α`, `g` over `β`, `h` over `γ`, for binary functions `m : δ → γ → ε`, `n : α → β → δ`, `m' : α → ε' → ε`, `n' : β → γ → ε'`, if for all `a` of type `α`, `b` of type `β`, `c` of type `γ`, the binary function `m` applied to the result of applying binary function `n` to `a` and `b`, and `c`, is equal to the application of binary function `m'` to `a` and the result of applying binary function `n'` to `b` and `c`, then the mapping of binary function `m` over the mapping of binary function `n` over filters `f` and `g`, and filter `h`, is equal to the mapping of binary function `m'` over filter `f` and the mapping of binary function `n'` over filters `g` and `h`. That is, the order in which these operations are performed does not affect the result.
More concisely: If for all `a : α`, `b : β`, `c : γ`, `m : δ → γ → ε`, `n : α → β → δ`, `m' : α → ε' → ε`, `n' : β → γ → ε'`, `m(n(a, b), c) = m'(a, n'(b, c))` implies `(m ∘ n)_f = m'_f ∘ (n'_g ∘ h)`, then the association of binary function mappings over filters `f`, `g`, and `h` holds.
|
Filter.map_map₂_right_comm
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' : δ → γ},
(∀ (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)
This theorem, `Filter.map_map₂_right_comm`, states that for any types `α`, `β`, `β'`, `γ`, and `δ`, any filters `f` and `g` on `α` and `β` respectively, any binary functions `m : α → β' → γ`, `m' : α → β → δ`, a function `n : β → β'` and a function `n' : δ → γ`, if for all `a` in `α` and `b` in `β`, `m` applied to `a` and `n` applied to `b` is equal to `n'` applied to `m'` applied to `a` and `b`, then the filter obtained by mapping the binary function `m` to the filter `f` and the filter obtained by mapping `n` to `g` is equal to the filter obtained by mapping `n'` to the filter obtained by mapping the binary function `m'` to the filter `f` and `g`. In essence, this theorem describes a certain commutativity property when mapping functions over filters.
More concisely: If `m(a, n(b)) = n'(m'(a, b))` for all `a` in `α` and `b` in `β`, then `(Filter.map f m).map g = Filter.map (Filter.map g m') n'`.
|
Filter.map₂_mono_right
theorem Filter.map₂_mono_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : Filter α} {g : Filter β},
f₁ ≤ f₂ → Filter.map₂ m f₁ g ≤ Filter.map₂ m f₂ g
The theorem `Filter.map₂_mono_right` states that for any types `α`, `β`, and `γ`, a binary function `m : α → β → γ`, two filters `f₁` and `f₂` on `α`, and a filter `g` on `β`, if `f₁` is a subfilter of `f₂` (i.e., `f₁ ≤ f₂`), then the image of the binary function `m` under the filter `f₁` and `g` is a subfilter of the image of `m` under the filter `f₂` and `g` (i.e., `Filter.map₂ m f₁ g ≤ Filter.map₂ m f₂ g`). This theorem essentially states a monotonicity property of the `map₂` operation with respect to the right argument.
More concisely: If `f₁ ≤ f₂` are filters on `α` and `γ` is a type, then the image of `f₁` under the function `m : α → β → γ` and filter `g` on `β`, `Filter.map₂ m f₁ g`, is a subfilter of the image of `f₂` under the same function and filter, `Filter.map₂ m f₂ g`.
|
Filter.map₂_pure_left
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
The theorem `Filter.map₂_pure_left` states that for any types `α`, `β`, `γ`, any binary function `m` from `α` and `β` to `γ`, any filter `g` of type `β` and any element `a` of type `α`, the image of the binary function `m` on the filter `pure a` (a filter that contains only `a`) and the filter `g` is the same as the image of the function `m a` (a function from `β` to `γ` obtained by fixing the first argument of `m` to `a`) on the filter `g`. In mathematical terms, this is saying that mapping a binary function over a singleton set and a filter is equivalent to mapping a unary function over the filter.
More concisely: For any binary function `m` and filter `g`, the image of `m` on the filter `pure a` and `g` is equal to the application of the unary function `x ↦ m a x` to `g`.
|
Filter.map_map₂_distrib_left
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' : α → α'},
(∀ (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
This theorem, named `Filter.map_map₂_distrib_left`, states that for all types `α`, `α'`, `β`, `γ`, and `δ`, and for all binary function `m : α → β → γ`, filters `f : Filter α` and `g : Filter β`, function `n : γ → δ`, binary function `m' : α' → β → δ`, and function `n' : α → α'`, if for all `a : α` and `b : β`, the function `n` applied to the result of `m` applied to `a` and `b` is equivalent to `m'` applied to `n'` of `a` and `b`, then the map of `n` over the map₂ of `m`, `f` and `g` equals the map₂ of `m'` over the map of `n'` on `f` and `g`.
In other words, it states a certain kind of commutativity and distributivity of the map and map₂ operations over filters, under the given function transformation conditions.
More concisely: If for all `a : α` and `b : β`, `n (m a b) = m' (n' a) (n' b)`, then `(Map.map n).map₂ (Map₂.map₂ m f g) = Map₂.map₂ (λ a b, m' (n' a) (n' b)) (Map.map (n') f) (Map.map (n') g)`.
|
Filter.map_map₂_antidistrib
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₂ : α → α'},
(∀ (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)
This theorem states that for any types `α`, `α'`, `β`, `β'`, `γ`, and `δ`; a binary function `m : α → β → γ`; two filters `f : Filter α` and `g : Filter β`; a unary function `n : γ → δ`; a reversed binary function `m' : β' → α' → δ`; and two unary functions `n₁ : β → β'` and `n₂ : α → α'`, if for every pair of elements `(a : α, b : β)`, the function `n` applied to the result of `m a b` equals the result of `m'` applied to `n₁ b` and `n₂ a`, then the filter obtained by mapping `n` over the filter obtained from mapping the binary function `m` over filters `f` and `g` equals the filter obtained by mapping the binary function `m'` over the filters obtained from mapping `n₁` over `g` and `n₂` over `f`.
More concisely: If for all `a : α` and `b : β`, `n(m a b) = m' (n₁ b) (n₂ a)` implies `(n ∘ f) = (m' ∘ (n₁ ∘ g) ∘ n₂) ∘ f`, then `(n ∘ (m ∘ (f × g))) = (m' ∘ (n₁ ∘ g) ∘ n₂) ∘ f`.
|
Filter.le_map₂_iff
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
The theorem `Filter.le_map₂_iff` states that for any types `α`, `β`, `γ`, a binary function `m : α → β → γ`, and the filters `f : Filter α`, `g : Filter β`, and `h : Filter γ`, filter `h` is less than or equal to the image of the binary function `m` applied to filters `f` and `g` if and only if for every set `s` in `f` and every set `t` in `g`, the image of the binary function `m` applied to `s` and `t` is in `h`.
In other words, this theorem specifies the condition necessary for filter `h` to be less than or equal to the image of a binary function applied to two other filters.
More concisely: For filters $f$ on type $\alpha$, $g$ on type $\beta$, and $h$ on type $\gamma$, and a binary function $m : \alpha \times \beta \to \gamma$, $h \leq \map{m}{f \times g}$ if and only if for all $s \in f$ and $t \in g$, $\map{m}{s,t} \in h$.
|
Filter.map₂_right_identity
theorem Filter.map₂_right_identity :
∀ {α : Type u_1} {β : Type u_3} {f : α → β → α} {b : β},
(∀ (a : α), f a b = a) → ∀ (l : Filter α), Filter.map₂ f l (pure b) = l
This theorem states that for any given types `α` and `β`, a binary function `f : α → β → α`, and an element `b : β`, if `b` serves as a right identity for the function `f` (i.e., for all `a` of type `α`, `f a b` equals `a`), then `pure b` also serves as a right identity for the operation `Filter.map₂ f` on any filter `l` of type `Filter α`. In other words, mapping the binary function `f` over the filter `l` and `pure b` results in the same filter `l`.
More concisely: For any filter `l` on type `α`, if element `b` is a right identity for binary function `f : α → β → α`, then `Filter.map₂ f l (pure b) = l`.
|
Filter.map_map₂_distrib
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₂ : β → β'},
(∀ (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)
This theorem, `Filter.map_map₂_distrib`, states that for all types `α`, `α'`, `β`, `β'`, `γ`, and `δ`, and for all functions `m` mapping from `α` and `β` to `γ`, `n` mapping from `γ` to `δ`, `m'` mapping from `α'` and `β'` to `δ`, and `n₁` and `n₂` mapping from `α` to `α'` and `β` to `β'` respectively, if for every `a` in `α` and `b` in `β`, applying `n` to `m(a, b)` is equal to applying `m'` to `n₁(a)` and `n₂(b)`, then the image of the function `n` under the filter `m` composed with `f` and `g` is equal to the image of the function `m'` under the filter `n₁` composed with `f` and `n₂` composed with `g`.
In mathematical terms, this theorem reflects the distributivity of function mapping over binary function mapping under certain conditions, when applied to filters on sets.
More concisely: If for all `a` in `α` and `b` in `β`, `n(m(a, b)) = m'(n₁(a), n₂(b))`, then `(filter m . f . g) . n = filter (λ a b, m'(n₁ a, n₂ b)) . f . g`.
|
Filter.map₂_bot_right
theorem Filter.map₂_bot_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α}, Filter.map₂ m f ⊥ = ⊥
The theorem `Filter.map₂_bot_right` states that for any types `α`, `β`, and `γ`, and any binary function `m` from `α` and `β` to `γ`, and any filter `f` on `α`, the image of the function `m` applied to the filter `f` and the bottom filter (i.e., the filter that contains no sets) is equal to the bottom filter.
In mathematical terms, if we think of the function `Filter.map₂ m f` as creating a new filter from `α × β` to `γ` by applying `m` to `f` and another filter, then if that other filter is the empty filter (denoted by `⊥`), the result is also the empty filter. This makes sense, because there are no elements in the empty filter to apply the function `m` to.
More concisely: For any filter `f` on type `α` and any binary function `m` from `α × β` to `γ`, `Filter.map₂ m (f × ⊥) = ⊥`, where `⊥` denotes the bottom filter on `γ`.
|
Filter.map₂_distrib_le_right
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' : α' → β' → ε},
(∀ (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)
This theorem, named `Filter.map₂_distrib_le_right`, states that for all types α, α', β, β', γ, δ, ε, filters `f` on α, `g` on β, `h` on γ, binary functions `m` from δ to γ to ε, `n` from α to β to δ, `m₁` from α to γ to α', `m₂` from β to γ to β', and `n'` from α' to β' to ε, if for each element `a` of type α, `b` of type β, and `c` of type γ, the result of applying `m` to the result of applying `n` to `a` and `b` and to `c` equals the result of applying `n'` to the result of applying `m₁` to `a` and `c` and to the result of applying `m₂` to `b` and `c`, then the filter obtained by applying the binary function `m` to the filter obtained from applying the binary function `n` to filters `f` and `g` and to filter `h` is less than or equal to the filter obtained by applying the binary function `n'` to the filter obtained from applying the binary function `m₁` to filters `f` and `h` and to the filter obtained from applying the binary function `m₂` to filters `g` and `h`. The comment mentions that the other direction does not hold because of the `h`-`h` cross terms on the RHS.
More concisely: If for all `a: α`, `b: β`, and `c: γ`, `m (n a b) c = n' (m₁ a c) (m₂ b c)`, then `m'' (Filter.map₂ n g) h ≤ Filters.map₂ n' (Filters.map₂ m₁ f h) (Filters.map₂ m₂ g h)`, where `m''` is the function obtained from `m` by applying `Filters.map₂` on the third argument `h`.
|
Filter.map₂_eq_bot_iff
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 = ⊥
The theorem `Filter.map₂_eq_bot_iff` states that for any types `α`, `β` and `γ`, and any function `m` from `α` and `β` to `γ`, and any Filters `f` on `α` and `g` on `β`, the image of the binary function `m` on Filters `f` and `g` being the bottom filter (the filter which contains all sets) is equivalent to either `f` being the bottom filter or `g` being the bottom filter. In mathematical terms, \(Filter.map₂(m, f, g) = ⊥\) if and only if \(f = ⊥\) or \(g = ⊥\).
More concisely: For any functions `m` from `α × β` to `γ` and filters `f` on `α` and `g` on `β` in Lean, `Filter.map₂(m, f, g) = ⊥` if and only if `f = ⊥` or `g = ⊥`.
|
Filter.NeBot.map₂
theorem Filter.NeBot.map₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
f.NeBot → g.NeBot → (Filter.map₂ m f g).NeBot
The theorem `Filter.NeBot.map₂` states that for any types `α`, `β`, and `γ`, and for any binary function `m : α → β → γ` and filters `f : Filter α` and `g : Filter β`, if the filters `f` and `g` are not bottom filters (meaning that they are not the filter that contains every set), then the image of the binary function `m` under the filters `f` and `g`, denoted as `Filter.map₂ m f g`, is also a non-bottom filter. In essence, the image of two non-bottom filters under a binary function remains a non-bottom filter.
More concisely: If filters `f` and `g` over types `α` and `β`, respectively, are non-bottom, then the image of their composition under a binary function `m : α → β → γ` is also a non-bottom filter over type `γ`.
|
Filter.map₂_neBot_iff
theorem Filter.map₂_neBot_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
(Filter.map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot
The theorem `Filter.map₂_neBot_iff` states that for any types `α`, `β`, and `γ`, and any binary function `m : α → β → γ`, and any filters `f : Filter α` and `g : Filter β`, the filter `Filter.map₂ m f g` is non-bottom if and only if both `f` and `g` are non-bottom. Here, a filter being non-bottom means that it is not the trivial filter, which contains only the empty set.
More concisely: For filters `f` on type `α` and `g` on type `β`, and binary function `m : α → β → γ`, `Filter.map₂ m f g` is non-empty if and only if both `f` and `g` are non-empty. (Note: In Lean, a non-bottom filter is the same as a non-empty filter.)
|
Filter.map₂_map_left
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
This theorem, `Filter.map₂_map_left`, states that for any function `m : γ → β → δ`, function `n : α → γ`, and filters `f : Filter α` and `g : Filter β` over the types `α` and `β` respectively, the image of the binary function `m` under the mapping of `n` on `f` and `g` is equal to the image of the binary function `(fun a b => m (n a) b)` under `f` and `g`. Essentially, it presents a property of preserving the binary function image under certain transformations, specifically when the transformation is applied on the left input of the binary function.
More concisely: For filters `f` over `α` and `g` over `β`, and any function `m : γ → β → δ`, the application of `m` to the images of `n` under `f` and `g` is equal to the application of the function `m . (n × id)` under `f` and `g`. (Here, `n : α → γ`, `id` is the identity function on `β`, and `×` denotes the product type.)
|
Filter.map_prod_eq_map₂
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
The theorem `Filter.map_prod_eq_map₂` states that for any types `α`, `β`, and `γ`, and for any binary function `m` from `α` and `β` to `γ`, and any filters `f` and `g` on `α` and `β` respectively, the forward map of the filter of the product of `f` and `g` under the function `m` applied to the components of the product is equal to the image of the binary function `m` as a function from the filters `f` and `g` to a filter on `γ`. This essentially states that the two ways of mapping a binary function over a product of filters give the same result.
More concisely: For any types `α`, `β`, and `γ`, and binary function `m` from `α × β` to `γ`, filters `f` on `α`, and `g` on `β`, the map of the product filter `f × g` under `m` equals the image filter of `m` on the pair `(f, g)`.
|
Filter.map₂_map_right
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
The theorem `Filter.map₂_map_right` states that for all types `α`, `β`, `γ`, `δ`, for any filters `f` of type `α` and `g` of type `β`, and for any functions `m : α → γ → δ` and `n : β → γ`, the image of the binary function `m` under the filter `f` and the mapped filter `n(g)` (denoted as `Filter.map₂ m f (Filter.map n g)`) is equal to the image of the binary function `(a, b) ↦ m a (n b)` under the filters `f` and `g` (denoted as `Filter.map₂ (fun a b => m a (n b)) f g`). In essence, it's saying that the mapping of the second filter can be "absorbed" into the binary function without changing the result.
More concisely: For any filters `f` and `g`, and functions `m` and `n`, `Filter.map₂ m (Filter.map n g) f = Filter.map₂ (λa b, m a (n b)) f g`.
|
Filter.NeBot.of_map₂_left
theorem Filter.NeBot.of_map₂_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
(Filter.map₂ m f g).NeBot → f.NeBot
The theorem `Filter.NeBot.of_map₂_left` states that for all types `α`, `β`, and `γ`, a binary function `m` mapping from `α` and `β` to `γ`, and two filters `f` and `g` on `α` and `β` respectively, if the image of the binary function `m` mapping from `f` and `g` to a filter in `γ` (represented by `Filter.map₂ m f g`) is not the bottom filter (meaning it's not the empty set), then `f` (the filter on `α`) is also not the bottom filter. In mathematical notation, this could be interpreted as: for all `α`, `β`, `γ`, `m : α → β → γ`, `f : Filter α`, and `g : Filter β`, if `Filter.map₂ m f g ≠ ∅`, then `f ≠ ∅`.
More concisely: If the composite filter of a function and two filters is non-empty, then each of the two filters is non-empty.
|
Filter.map₂_pure_right
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
The theorem `Filter.map₂_pure_right` asserts that for any types `α`, `β`, and `γ`, a binary function `m : α → β → γ`, a filter `f` on type `α`, and a value `b` of type `β`, the image of the binary function `m` applied to the filter `f` and the pure filter containing only `b` is equivalent to the image of the function `m x b` applied to the filter `f`. In mathematical terms, this theorem demonstrates a kind of "compatability" between the binary function and the filter map with the special case of a pure filter.
More concisely: For any type `α`, filter `f` on `α`, function `m : α -> beta -> gamma`, and value `b` of type `β`, the image of `m` applied to `f` and the pure filter at `b` is equal to the image of `m x b` applied to `f`.
|
Filter.map_map₂_antidistrib_right
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' : α → α'},
(∀ (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)
The theorem `Filter.map_map₂_antidistrib_right` states that for any types `α`, `β`, `γ`, `δ`, `α'`, any binary function `m : α → β → γ`, any filters `f : Filter α` and `g : Filter β`, any function `n : γ → δ`, any binary function `m' : β → α' → δ`, and any function `n' : α → α'`, if for all elements `a : α` and `b : β`, the function `n` applied to the result of function `m` applied to `a` and `b` equals to the function `m'` applied to `b` and `n'` applied to `a` (`n (m a b) = m' b (n' a)`), then the forward map of the filter `n` applied to the image of the binary function `m` as a function `Filter α → Filter β → Filter γ` is equal to the image of the binary function `m'` as a function `Filter β → Filter α' → Filter δ` where the filter `n'` is applied to `Filter α`.
This theorem provides a kind of distribution law for the interaction between the function `n` and the binary function `m` in the context of filter mapping.
More concisely: If for all `a : α` and `b : β`, `n (m a b) = m' b (n' a)`, then `(Filter.map₂ m)(n) = n' ''' (Filter.map₂ m'*)(g) (f)` where `*` denotes the dual filter operator.
|
Filter.map₂_mono_left
theorem Filter.map₂_mono_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g₁ g₂ : Filter β},
g₁ ≤ g₂ → Filter.map₂ m f g₁ ≤ Filter.map₂ m f g₂
The theorem `Filter.map₂_mono_left` states that for any types `α`, `β`, and `γ` and any binary function `m : α → β → γ`, if we have two filters `g₁` and `g₂` on `β` such that `g₁` is a subset of `g₂` (or equivalently, `g₁` is finer than `g₂`), then the image of `m` under the filter `f` on `α` and `g₁` is a subset of the image of `m` under `f` and `g₂`. In other words, increasing the coarseness of the filter on the second argument of `m` (from `g₁` to `g₂`) does not decrease the coarseness of the resulting filter on `γ` (from `Filter.map₂ m f g₁` to `Filter.map₂ m f g₂`). This theorem captures a form of monotonicity of the `Filter.map₂` function with respect to its second filter argument.
More concisely: If `f` is a filter on `α`, `g₁` and `g₂` are filters on `β` with `g₁ ⊆ g₂`, then `Filter.map₂ m f g₁ ⊆ Filter.map₂ m f g₂` for any binary function `m : α → β → γ`.
|
Filter.map₂_distrib_le_left
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' : β' → γ' → ε},
(∀ (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 theorem `Filter.map₂_distrib_le_left` is about a certain inequality between filters and maps. Specifically, for all types `α`, `β`, `β'`, `γ`, `γ'`, `δ`, and `ε`, and for all filters `f`, `g`, and `h` over these types, as well as maps `m`, `n`, `m₁`, `m₂`, and `n'`, if for every `a` from `α`, `b` from `β`, and `c` from `γ` the function `m` applied to `a` and the result of applying `n` to `b` and `c` equals applying `n'` to the result of applying `m₁` to `a` and `b` and the result of applying `m₂` to `a` and `c`, then the image of the binary function `m` under the filter `f` and the image of the binary function `n` under the filters `g` and `h` is less than or equal to the image of the binary function `n'` under the image of the binary function `m₁` under the filters `f` and `g`, and the image of the binary function `m₂` under the filters `f` and `h`.
In mathematical terms, if two composed functions are equal, then the image of one function under certain filters is less than or equal to the image of the other function under different filters. This theorem does not guarantee the opposite direction due to the `f-f` cross terms on the right-hand side.
More concisely: If `m(a, b) = n(m₁(a, b), m₂(a, c))` for all `a: α`, `b: β`, and `c: γ`, then `(Filter.map₂ m f g).map n ≤ n' ((Filter.map₂ m₁ f g) ⊓ Filter.map₂ m₂ f h)`.
|
Filter.NeBot.of_map₂_right
theorem Filter.NeBot.of_map₂_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
(Filter.map₂ m f g).NeBot → g.NeBot
This theorem states that for any types `α`, `β`, and `γ`, and for any binary function `m` from `α` and `β` to `γ`, and any filters `f` on `α` and `g` on `β`, if the filter obtained by mapping `m` over `f` and `g` (denoted as `Filter.map₂ m f g`) is not the bottom filter (i.e., it is not the trivial filter that contains all sets), then the filter `g` itself is also not the bottom filter. In other words, a non-trivial image filter implies a non-trivial original filter.
More concisely: If `Filter.map₂ m (non-bot f) (non-bot g)` holds in Lean, then `non-bot g` also holds. Here, `m` is a binary function from types `α` and `β` to `γ`, `f` is a filter on `α`, `g` is a filter on `β`, and `non-bot` denotes a non-bottom filter.
|
Filter.map_map₂_antidistrib_left
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' : β → β'},
(∀ (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
This theorem, `Filter.map_map₂_antidistrib_left`, states that for any types `α`, `β`, `β'`, `γ`, and `δ`, given a binary function `m: α → β → γ`, a function `n: γ → δ`, a function `n': β → β'`, a function `m': β' → α → δ`, and filters `f : Filter α` and `g : Filter β`, if for all `a` in `α` and `b` in `β`, the function `n` applied to `m a b` equals the function `m'` applied to `n' b` and `a`, then the map of `n` on the map₂ of `m`, `f`, and `g` is equal to the map₂ of `m'`, the map of `n'` on `g`, and `f`.
In mathematical terms, this can be thought of as a sort of distributive property for mapping operations on filters.
More concisely: If for all `a` in `α` and `b` in `β`, `n (m a b) = m' (n' b) a`, then `(Filter.map₂ m f g) = (Filter.map₂ m' (Filter.map n g) f)`.
|
Filter.map_map₂_right_anticomm
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' : δ → γ},
(∀ (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)
The theorem `Filter.map_map₂_right_anticomm` states that for any types `α`, `β`, `β'`, `γ`, and `δ`, any filters `f` on `α` and `g` on `β`, any binary functions `m : α → β' → γ`, `m' : β → α → δ`, and any functions `n : β → β'`, `n' : δ → γ`, if for all `a` in `α` and `b` in `β` the function `m` applied to `a` and `n` applied to `b` equals `n'` applied to `m'` applied to `b` and `a`, then the image of the binary function `m` under the filters `f` and the image of the filter `g` under `n` equals the image of `n'` under the image of the binary function `m'` under `filters` `g` and `f`.
In mathematical terms, this means that we can switch the order of filter mapping and binary function mapping under certain conditions, allowing us to rearrange filter and function operations without changing the result.
More concisely: If `m(a, b) = n'(m'(b, a))` for all `a` in `α` and `b` in `β`, then `(Filter.map f m).map g = Filter.map (n' ∘ m') (g ∘ f)`.
|