Filter.map_const_principal_coprod_map_id_principal
theorem Filter.map_const_principal_coprod_map_id_principal :
∀ {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι),
(Filter.map (fun x => b) (Filter.principal {a})).coprod (Filter.map id (Filter.principal {i})) =
Filter.principal ({b} ×ˢ Set.univ ∪ Set.univ ×ˢ {i})
This theorem, `Filter.map_const_principal_coprod_map_id_principal`, characterizes the coproduct of the mappings of two principal filters, `𝓟 {a}` and `𝓟 {i}`. The first filter `𝓟 {a}` is mapped under the constant function `fun a => b` and the second filter `𝓟 {i}` is mapped under the identity function. For any given types `α`, `β`, and `ι`, and any given elements `a` of type `α`, `b` of type `β`, and `i` of type `ι`, the theorem states that the coproduct of these two mappings equals the principal filter of the set that includes all possible ordered pairs where the first element is `b` and the second element is any element of type `ι`, in addition to all possible ordered pairs where the first element is any element of type `α` and the second element is `i`. This theorem, combined with the following lemma `map_prod_map_const_id_principal_coprod_principal`, illustrates an example where the inequality in the lemma `map_prod_map_coprod_le` can be strict.
More concisely: The coproduct of the constant mapping of a principal filter to `b` and the identity mapping of another principal filter is equivalent to the principal filter generated by pairs of the form `(b, i)` and `(a, i)` for any types `α`, `β`, `ι`, elements `a ∈ α`, `b ∈ β`, and `i ∈ ι`.
|
Filter.prod_mono
theorem Filter.prod_mono :
∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ := by
sorry
The theorem `Filter.prod_mono` states that for all types `α` and `β`, and for all pairs of filters `(f₁, f₂)` on `α` and `(g₁, g₂)` on `β`, if `f₁` is a sub-filter of `f₂` and `g₁` is a sub-filter of `g₂`, then the product filter `f₁ ×ˢ g₁` is a sub-filter of the product filter `f₂ ×ˢ g₂`.
In other words, if we have filters `f₁` and `f₂` on type `α` and filters `g₁` and `g₂` on type `β`, and if `f₁` is contained in `f₂` and `g₁` is contained in `g₂`, then the product of `f₁` and `g₁` is contained in the product of `f₂` and `g₂`. The product of two filters is a filter on the product of the respective types.
More concisely: Given filters `f₁` on `α` and `g₁` on `β`, if `f₁` is a sub-filter of `f₂` and `g₁` is a sub-filter of `g₂`, then the product filter `f₁ × g₁` is a sub-filter of `f₂ × g₂`.
|
Filter.prod_mem_prod
theorem Filter.prod_mem_prod :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : Filter α} {g : Filter β},
s ∈ f → t ∈ g → s ×ˢ t ∈ f ×ˢ g
This theorem states that for any types `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, along with filters `f` on `α` and `g` on `β`, if `s` is in `f` and `t` is in `g`, then the Cartesian product of `s` and `t` is in the Cartesian product of `f` and `g`. In other words, it says that the product of two sets is a member of the product of their respective filters if the individual sets are members of their respective filters.
More concisely: For filters \(f\) on type \(\alpha\) and \(g\) on type \(\beta\), if \(s \in f\) (where \(s\) is a set of type \(\alpha\)) and \(t \in g\) (where \(t\) is a set of type \(\beta\)), then \(s \times t \in f \times g\) (where \(s \times t\) is the Cartesian product of \(s\) and \(t\)).
|
Filter.Eventually.prod_mk
theorem Filter.Eventually.prod_mk :
∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {pa : α → Prop},
(∀ᶠ (x : α) in la, pa x) →
∀ {lb : Filter β} {pb : β → Prop}, (∀ᶠ (y : β) in lb, pb y) → ∀ᶠ (p : α × β) in la ×ˢ lb, pa p.1 ∧ pb p.2
This theorem, `Filter.Eventually.prod_mk`, states that for any types `α` and `β`, any filters `la` on `α` and `lb` on `β`, and any properties `pa` on `α` and `pb` on `β`, if almost all elements `x` in the filter `la` satisfy property `pa` and almost all elements `y` in the filter `lb` satisfy property `pb`, then almost all pairs `(p : α × β)` in the product filter `la ×ˢ lb` satisfy both properties `pa` on the first element and `pb` on the second element. Here, "almost all" is described by the `∀ᶠ` symbol, which means "eventually for all" or "for all outside a set of measure zero" in the context of filters.
More concisely: If filters `la` on `α` and `lb` on `β` have almost all elements satisfying properties `pa` and `pb` respectively, then the product filter `la ×ˢ lb` has almost all pairs satisfying both `pa` and `pb`.
|
Filter.prod_comap_comap_eq
theorem Filter.prod_comap_comap_eq :
∀ {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁}
{m₂ : β₂ → α₂}, Filter.comap m₁ f₁ ×ˢ Filter.comap m₂ f₂ = Filter.comap (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
This theorem states that for any two types `α₁` and `α₂`, with filters `f₁` and `f₂`, and for any two mappings `m₁` from `β₁` to `α₁` and `m₂` from `β₂` to `α₂`, the cartesian product of the comap (preimage) of `f₁` under `m₁` and the comap of `f₂` under `m₂` is equal to the comap of the cartesian product filter `f₁ ×ˢ f₂` under a function that applies `m₁` to the first element of a pair and `m₂` to the second.
In other words, the theorem demonstrates a property of filter comaps with respect to the cartesian product: pulling back the filters along the mappings before forming the product is the same as forming the product first and then pulling back along the pair of mappings.
More concisely: For any filters `f₁` on type `α₁`, `f₂` on type `α₂`, and mappings `m₁` from `β₁` to `α₁` and `m₂` from `β₂` to `α₂`, the comap of the cartesian product filter `f₁ ×ˢ f₂` under the function `λ (x, y) => (m₁ x, m₂ y)` is equal to the cartesian product of the comaps of `f₁` under `m₁` and `f₂` under `m₂`.
|
Filter.Eventually.curry
theorem Filter.Eventually.curry :
∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop},
(∀ᶠ (x : α × β) in la ×ˢ lb, p x) → ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
This theorem states that for any given types `α` and `β`, and any given filters `la` on type `α` and `lb` on type `β`, if a certain property `p` holds eventually (i.e., outside a finite set) for pairs `(x, y)` drawn from `α` and `β` under the Cartesian product of `la` and `lb`, then it also holds that eventually, for any `x` drawn from `α` under `la`, the property `p` holds eventually for all `y` drawn from `β` under `lb`. In other words, if a property holds eventually for all pairs from two filters' Cartesian product, then the property also holds when we separate the components and consider them under their original filters.
More concisely: If a property holds eventually for all pairs in the product of two filters, then the property holds eventually for each filter's elements when considering their respective projections.
|
Mathlib.Order.Filter.Prod._auxLemma.7
theorem Mathlib.Order.Filter.Prod._auxLemma.7 :
∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : Filter α} {g : Filter β},
(s ∈ f ×ˢ g) = ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
This theorem is about the product of two filters. It says that for any two types `α` and `β`, a set `s` of pairs `(α, β)`, and filters `f` and `g` over `α` and `β` respectively, the set `s` is in the product of `f` and `g` if and only if there exist subsets `t₁` and `t₂` in `f` and `g` respectively, such that the product of `t₁` and `t₂` is a subset of `s`. In mathematical terms, given a set `s` in the Cartesian product of `α` and `β`, and filters `f` on `α` and `g` on `β`, `s` belongs to the product filter `f ×ˢ g` if and only if there exist `t₁` in `f` and `t₂` in `g` such that the Cartesian product of `t₁` and `t₂` is contained in `s`.
More concisely: A set of pairs in the Cartesian product of two types belongs to the product filter of two filters if and only if there exist subsets in each filter whose Cartesian product contains the set.
|
Filter.map_swap4_prod
theorem Filter.map_swap4_prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter α} {g : Filter β} {h : Filter γ}
{k : Filter δ}, Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
This theorem, named `Filter.map_swap4_prod`, states that for any types `α`, `β`, `γ`, `δ` and any filters `f` on `α`, `g` on `β`, `h` on `γ`, and `k` on `δ`, the operation of mapping a four-tuple from the product filter `(f ×ˢ g) ×ˢ h ×ˢ k` so that the first and third elements switch places with the second and fourth elements respectively, yields the same result as directly taking the product filter `(f ×ˢ h) ×ˢ g ×ˢ k`. In other words, it demonstrates a specific kind of commutativity property for this mapping operation on product filters.
More concisely: For any filters \(f\) on \(\alpha\), \(g\) on \(\beta\), \(h\) on \(\gamma\), and \(k\) on \(\delta\), the filter operations \((f \times g) \times h \times k\) and \(f \times h \times g \times k\) yield the same result when swapping the second and third elements.
|
Filter.tendsto_prod_iff'
theorem Filter.tendsto_prod_iff' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {g' : Filter γ} {s : α → β × γ},
Filter.Tendsto s f (g ×ˢ g') ↔ Filter.Tendsto (fun n => (s n).1) f g ∧ Filter.Tendsto (fun n => (s n).2) f g'
The theorem `Filter.tendsto_prod_iff'` states that for all filters `f` over a type `α`, `g` over a type `β`, and `g'` over a type `γ`, and for all functions `s` from `α` to the cartesian product of `β` and `γ`, the function `s` tends to the product filter `g ×ˢ g'` if and only if the first component of `s` tends to `g` and the second component of `s` tends to `g'`. In other words, this theorem characterizes the limit of a function towards a product of filters in terms of the limits of the individual components of the function.
More concisely: For any filters $f$ over type $\alpha$, $g$ over type $\beta$, and $g'$ over type $\gamma$, and any function $s$ from $\alpha$ to the cartesian product $β × γ$, $s$ tends to the product filter $g ×ˢ g'$ if and only if the first component of $s$ tends to $g$ and the second component of $s$ tends to $g'$.
|
Filter.prod_pure_pure
theorem Filter.prod_pure_pure : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, pure a ×ˢ pure b = pure (a, b) := by
sorry
This theorem, `Filter.prod_pure_pure`, states that for all types `α` and `β`, and for all values `a` of type `α` and `b` of type `β`, the product of the filters `pure a` and `pure b` is equal to the filter `pure (a, b)`. In other words, it asserts the equality between the filter of the product of two pure values, and the pure filter of the pair of these values.
More concisely: For all types `α` and `β`, and for all `a : α` and `b : β`, the filters `pure a` and `pure b` over their respective types have product equal to the filter `pure (a, b)` over their cartesian product type `α × β`.
|
Filter.Eventually.diag_of_prod_left
theorem Filter.Eventually.diag_of_prod_left :
∀ {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop},
(∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
The theorem `Filter.Eventually.diag_of_prod_left` states that for any types `α` and `γ`, any filters `f` on `α` and `g` on `γ`, and any property `p` on the cartesian product of `α × α` and `γ`, if `p` holds almost everywhere (except on a set of measure zero) on the product filter `(f ×ˢ f) ×ˢ g`, then `p` also holds almost everywhere on the product filter `f ×ˢ g`, when the first component of the tuples in `α × γ` is duplicated. In other words, it ensures that if a property is almost always true when considering pairs from the first filter, it remains true when we only consider the same elements from the first filter.
More concisely: If a property holds almost everywhere on the product of two filters with the first component repeated, then it also holds almost everywhere on their product filter.
|
Filter.map_snd_prod
theorem Filter.map_snd_prod :
∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [inst : f.NeBot], Filter.map Prod.snd (f ×ˢ g) = g
This theorem states that for all types `α` and `β`, given a filter `f` of type `α` and a filter `g` of type `β`, if `f` is a proper (non-bottom) filter, then the filter obtained by mapping the function `Prod.snd` (which projects out the second component of a pair) over the filter product of `f` and `g` is equal to `g`. In other words, it extracts the second component of the filter product, effectively "ignoring" the first.
More concisely: For all filters $f$ on type $\alpha$ and $g$ on type $\beta$, if $f$ is proper, then $(f \times g).\text{snd} = g$.
|
Mathlib.Order.Filter.Prod._auxLemma.31
theorem Mathlib.Order.Filter.Prod._auxLemma.31 :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, (f ×ˢ g = ⊥) = (f = ⊥ ∨ g = ⊥)
This theorem states that for any two types `α` and `β`, and any two filters `f` and `g` on these types, the product filter `f ×ˢ g` is the bottom element (denoted by `⊥`, which can be thought of as the "smallest" filter) if and only if either `f` or `g` is the bottom element. In other words, the product of two filters is the smallest possible filter if and only if at least one of the filters is the smallest possible filter.
More concisely: For filters \(f\) and \(g\) on types \(\alpha\) and \(\beta\) respectively, \(f \times_\bot g = \bot\) if and only if \(f = \bot\) or \(g = \bot\).
|
Filter.frequently_prod_and
theorem Filter.frequently_prod_and :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α → Prop} {q : β → Prop},
(∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b
The theorem `Filter.frequently_prod_and` states that for any types `α` and `β`, filters `f` and `g` on these types, and propositions `p` and `q` that apply to elements of these types respectively, the proposition `p ∧ q` frequently occurs along the product of these two filters if and only if `p` frequently occurs along the filter `f` and `q` frequently occurs along the filter `g`. Here, "frequently" means that the set of elements satisfying the proposition is dense in the filter, i.e., every neighborhood of every point in the filter contains an element satisfying the proposition.
More concisely: For filters `f` and `g` on types `α` and `β` respectively, and propositions `p : α → Prop` and `q : β → Prop`, the proposition `∀x ∈ f, ∃y ∈ g, p x ∧ q y` is dense in `f × g` if and only if `p` is dense in `f` and `q` is dense in `g`.
|
Filter.prod_map_map_eq'
theorem Filter.prod_map_map_eq' :
∀ {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁)
(G : Filter β₁), Filter.map f F ×ˢ Filter.map g G = Filter.map (Prod.map f g) (F ×ˢ G)
The theorem `Filter.prod_map_map_eq'` states that for any types `α₁`, `α₂`, `β₁`, `β₂`, any functions `f : α₁ → α₂` and `g : β₁ → β₂`, and any filters `F` on `α₁` and `G` on `β₁`, the product filter of mapping `f` on `F` and mapping `g` on `G` is equal to the filter obtained by mapping the function `Prod.map f g` on the product filter of `F` and `G`. In other words, the theorem describes a certain commutative property of filter mapping with respect to the product operation on filters.
More concisely: For any filters $F$ on type $\alpha\_1$ and $G$ on type $\beta\_1$, and any functions $f : \alpha\_1 \to \alpha\_2$ and $g : \beta\_1 \to \beta\_2$, the filter obtained by applying $f$ to the product filter of $F$ and $G$ is equal to the product filter of $f$ and $g$, i.e., $(f \times g)(F \otimes G) = (\text{Prod.map } f \ g)(F \otimes G)$.
|
Filter.prod_pure
theorem Filter.prod_pure :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {b : β}, f ×ˢ pure b = Filter.map (fun a => (a, b)) f
This theorem states that for any filter `f` of type `α` and an element `b` of type `β`, the Cartesian product of `f` and the singleton set `{b}` (expressed as `pure b`) is equal to the filter obtained by mapping each element `a` in `f` to the pair `(a, b)`. In other words, all the elements in the resulting filter are pairs where the first component comes from the original filter and the second component is the fixed element `b`.
More concisely: For any filter `f` on type `α` and element `b` of type `β`, the filters `{a | ∃ x, (a, b) ∈ f} × {pure b}` and `{a, b | a ∈ f}` are equal.
|
Filter.map_prod_map_const_id_principal_coprod_principal
theorem Filter.map_prod_map_const_id_principal_coprod_principal :
∀ {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι),
Filter.map (Prod.map (fun x => b) id) ((Filter.principal {a}).coprod (Filter.principal {i})) =
Filter.principal ({b} ×ˢ Set.univ)
This theorem characterizes the transformation, under the `Filter.map` operation, of the coproduct of two principle filters, `𝓟 {a}` and `𝓟 {i}`, under the `Prod.map` of two functions. The two functions are respectively the constant function `fun a => b` and the identity function. The result of this transformation equates to the principal filter of the cartesian product of the set `{b}` and the universal set. This theorem, along with the preceding lemma `map_const_principal_coprod_map_id_principal`, demonstrates that the inequality in the lemma `map_prod_map_coprod_le` can be strict.
More concisely: The `Filter.map` operation of the constant function `fun a => b` and the identity function on the coproduct of two principal filters `𝓟 {a}` and `𝓟 {i}` results in the principal filter of the cartesian product of `{b}` and the universal set.
|
Filter.tendsto_fst
theorem Filter.tendsto_fst :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.Tendsto Prod.fst (f ×ˢ g) f
The theorem `Filter.tendsto_fst` states that for any types `α` and `β` and for any filters `f : Filter α` and `g : Filter β`, the first projection function `Prod.fst` tends to `f` when taking the product filter `f ×ˢ g`. In other words, for each neighborhood of `f`, the pre-image under `Prod.fst` of that neighborhood is a neighborhood in the product filter `f ×ˢ g`. This is a formalization of the intuitive idea that when you project a product of topological spaces onto one of the factors, you preserve the limit properties of the filter basis.
More concisely: Given filters `f` on type `α` and `g` on type `β`, the first projection function `Prod.fst` is a continuous map from the product filter `f ×ˢ g` to `f`.
|
Filter.map_fst_prod
theorem Filter.map_fst_prod :
∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [inst : g.NeBot], Filter.map Prod.fst (f ×ˢ g) = f
The theorem `Filter.map_fst_prod` states that for any two types `α` and `β`, and any two filters `f : Filter α` and `g : Filter β`, if `g` is a filter not equal to the bottom filter (i.e., a filter that does not contain all sets), then the forward map of the filter of the product `f ×ˢ g` under the function `Prod.fst`, which projects an element of the product to its first component, is equal to `f`. In other words, projecting the product filter `f ×ˢ g` to its first component results in the original filter `f`, given that the second component filter `g` is not a bottom filter. This theorem states a key property of filters in the context of product spaces and projection operations.
More concisely: For any filters `f` on type `α` and `g` on type `β` with `g ≠ ⊥`, the forward image of `f ×ˢ g` under `Prod.fst` is equal to `f`.
|
Filter.Tendsto.prod_map
theorem Filter.Tendsto.prod_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
{c : Filter γ} {d : Filter δ},
Filter.Tendsto f a c → Filter.Tendsto g b d → Filter.Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
The theorem `Filter.Tendsto.prod_map` in Lean 4 states that for any types `α`, `β`, `γ`, and `δ`, and for any functions `f : α → γ` and `g : β → δ`, alongside with filters `a` on `α`, `b` on `β`, `c` on `γ` and `d` on `δ`, if `f` tends to `c` along `a` and `g` tends to `d` along `b`, then the function `Prod.map f g` that applies `f` to the first component and `g` to the second component of a pair, tends to the product filter `c ×ˢ d` along the product filter `a ×ˢ b`. In other words, if each function tends individually towards their respective filters, then the product function tends towards the product of the filters when applied to a pair of inputs.
More concisely: If functions `f : α → γ` and `g : β → δ` tend to filters `c` and `d`, respectively, then `Prod.map f g` tends to the product filter `c ×ˢ d`.
|
Filter.prod_comm
theorem Filter.prod_comm :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = Filter.map (fun p => (p.2, p.1)) (g ×ˢ f)
The theorem `Filter.prod_comm` states that for any types `α` and `β` and any filters `f` of type `α` and `g` of type `β`, the product of `f` and `g` is equal to the result of mapping the function that swaps the components of a pair over the product of `g` and `f`. In other words, the order of the filters in the product does not matter as long as we correspondingly adjust the order in the pairs of the resulting filter.
More concisely: For any filters $f$ on type $\alpha$ and $g$ on type $\beta$, we have $f \times g = g \times f := \{ (x, y) \mid (x, y) \in f \times g \land (y, x) \in g \times f \}$.
|
Filter.prod_map_map_eq
theorem Filter.prod_map_map_eq :
∀ {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁}
{m₂ : α₂ → β₂}, Filter.map m₁ f₁ ×ˢ Filter.map m₂ f₂ = Filter.map (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
The theorem `Filter.prod_map_map_eq` states that for any types `α₁`, `α₂`, `β₁`, `β₂`, any filters `f₁` on `α₁` and `f₂` on `α₂`, and any functions `m₁` from `α₁` to `β₁` and `m₂` from `α₂` to `β₂`, the product filter of the mappings `m₁` and `m₂` applied to filters `f₁` and `f₂` respectively, is equal to the filter mapped by a function that takes a pair and maps its elements using `m₁` and `m₂`, applied to the product filter of `f₁` and `f₂`. In other words, the process of filtering and then mapping commutes with the process of mapping and then filtering, when dealing with product filters.
More concisely: Given filters $f\_1$ on $\alpha\_1$, $f\_2$ on $\alpha\_2$, and functions $m\_1:\alpha\_1\to\beta\_1$, $m\_2:\alpha\_2\to\beta\_2$, the filters $m\_1\circ(f\_1\times f\_2)$ and $(m\_1\times m\_2)(\{ (x\_1,x\_2)\in\alpha\_1\times\alpha\_2 \mid x\_1\in f\_1 \} \times \{ y\_2\in\alpha\_2 \mid y\_2\in f\_2 \} )$ are equal.
|
Filter.Tendsto.prod_mk
theorem Filter.Tendsto.prod_mk :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m₁ : α → β}
{m₂ : α → γ}, Filter.Tendsto m₁ f g → Filter.Tendsto m₂ f h → Filter.Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h)
The theorem `Filter.Tendsto.prod_mk` states that if we have two functions `m₁` and `m₂` from a type `α` to types `β` and `γ` respectively, and if `m₁` tends to `g` with respect to a filter `f` on `α` and `m₂` tends to `h` with the same filter, then the function that maps `x` to the pair `(m₁ x, m₂ x)` also tends to the product filter `(g ×ˢ h)` with respect to `f`.
In other words, if for all neighborhoods of `g` and `h`, the pre-images under `m₁` and `m₂` respectively are neighborhoods of the filter `f`, then for all neighborhoods of `g ×ˢ h`, the pre-image under the function mapping `x` to `(m₁ x, m₂ x)` is also a neighborhood of `f`. This is a formalization of the concept of 'limit of a function' in the context of filters.
More concisely: If functions `m₁ : α → β` and `m₂ : α → γ` tend to `g : β` and `h : γ` respectively with respect to a filter `f` on `α`, then the function mapping `x` to `(m₁ x, m₂ x)` tends to the product `g × h` with respect to `f`.
|
Filter.eventually_prod_iff
theorem Filter.eventually_prod_iff :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α × β → Prop},
(∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
This theorem states that for any two types `α` and `β`, any two filters `f` and `g` on these types respectively, and any property `p` of pairs of elements from `α` and `β`, the property `p` holds eventually (i.e., outside of a finite number of exceptions) for pairs `(x, y)` drawn from the filters `f` and `g` if and only if there exist properties `pa` and `pb` such that `pa` holds eventually for elements `x` drawn from `f`, `pb` holds eventually for elements `y` drawn from `g`, and for any `x` that satisfies `pa` and any `y` that satisfies `pb`, the pair `(x, y)` satisfies `p`.
More concisely: For filters `f` on type `α` and `g` on type `β`, and any property `p` of pairs from `α × β`, `p` holds eventually for pairs drawn from `f` and `g` if and only if there exist properties `pa` and `pb` such that `pa` holds eventually for elements of `f` and `pb` holds eventually for elements of `g`, and for all `x` satisfying `pa` and `y` satisfying `pb`, `(x, y)` satisfies `p`.
|
Mathlib.Order.Filter.Prod._auxLemma.8
theorem Mathlib.Order.Filter.Prod._auxLemma.8 :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {t : Set β}, (t ∈ Filter.map m f) = (m ⁻¹' t ∈ f)
This theorem, named `Mathlib.Order.Filter.Prod._auxLemma.8`, states that for any types `α` and `β`, any filter `f` on `α`, any function `m` from `α` to `β`, and any set `t` of elements of type `β`, the set `t` is in the image of the filter `f` under the function `m` if and only if the preimage of `t` under `m` is in the filter `f`. In other words, it provides a criterion for a set to be in the image of a filter under a function: it is in the image if and only if its preimage is in the original filter.
More concisely: For any filter \(f\) on type \(\alpha\), function \(m:\alpha \rightarrow \beta\), and set \(t \subseteq \beta\), \(t\) is in the image of \(f\) under \(m\) if and only if \(m^{-1}(t) \in f\).
|
Filter.prod_inf_prod
theorem Filter.prod_inf_prod :
∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β},
f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
This theorem states that for any two pairs of filters (`f₁`, `g₁`) and (`f₂`, `g₂`) where filters are defined over arbitrary types `α` and `β`, the product of the infimum (or intersection) of the two filter pairs is equal to the infimum of their individual products. In more mathematical terms, `(f₁ × g₁) ∩ (f₂ × g₂) = (f₁ ∩ f₂) × (g₁ ∩ g₂)`. This means if you first combine the filters from each type and then take the intersection, it's the same as if you first take the intersection within each type and then combine the results.
More concisely: The infimum of the product of two filters (`f₁ × g₁`) is equal to the product of their infima (`(f₁ ∩ f₂) × (g₁ ∩ g₂)`).
|
Filter.prod_eq
theorem Filter.prod_eq :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = (Filter.map Prod.mk f).seq g
This theorem states that for any two types `α` and `β`, and any two filters `f` on `α` and `g` on `β`, the product filter of `f` and `g` is equivalent to the sequence filter of the map filter of the product constructor `Prod.mk` with respect to `f`, followed by `g`. In other words, it's saying that forming a product of two filters can be done either directly or by first mapping each element in the first filter to a function that attaches it to an element in the second filter, and then sequencing these functions over the second filter.
More concisely: For any filters `f` on type `α` and `g` on type `β`, the product filter of `f` and `g` is equal to the sequence filter of the map filter of the product constructor `Prod.mk` from `α × β` to `β`, applied to `g`, and then composed with the map filter of `f` on `α`.
|
Filter.tendsto_snd
theorem Filter.tendsto_snd :
∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.Tendsto Prod.snd (f ×ˢ g) g
The theorem `Filter.tendsto_snd` states that for all types `α` and `β`, and for any filters `f` of `α` and `g` of `β`, the function `Prod.snd` (which takes a pair and returns its second element) tends to `g` when applied to the Cartesian product of `f` and `g`. In other words, for every neighborhood of `g`, the preimage of this neighborhood under the function `Prod.snd` is a neighborhood of the Cartesian product filter `f ×ˢ g`. This describes the behavior of the second projection function on the product of two filters.
More concisely: For all filters $f$ on type $\alpha$ and $g$ on type $\beta$, the second projection function `Prod.snd` tends to $g$ when applied to the Cartesian product of $f$ and $g$, i.e., the preimage of every neighborhood of $g$ under `Prod.snd` is a neighborhood of $f \times g$.
|
Filter.pure_prod
theorem Filter.pure_prod :
∀ {α : Type u_1} {β : Type u_2} {a : α} {f : Filter β}, pure a ×ˢ f = Filter.map (Prod.mk a) f
The theorem `Filter.pure_prod` states that for any given types `α` and `β`, any element `a` of type `α`, and any filter `f` on type `β`, the product of the singleton set `{a}` and the filter `f` is equivalent to the filter obtained by applying the function `Prod.mk a` (which pairs `a` with each element of `f`) to `f`. In other words, pairing each element of a filter with a fixed element using the product operation is the same as mapping the pair-making function over the filter.
More concisely: For any types `α` and `β`, the filter obtained by applying the product operation to the singleton set `{a}` and a filter `f` on `β` is equal to the filter obtained by mapping the pairing function `Prod.mk a` over `f`.
|
Filter.mem_prod_iff
theorem Filter.mem_prod_iff :
∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : Filter α} {g : Filter β},
s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
This theorem states that for any types `α` and `β`, any set `s` of pairs `(α, β)`, and any filters `f` on `α` and `g` on `β`, the set `s` is in the product filter of `f` and `g` if and only if there exist subsets `t₁` and `t₂` in `f` and `g` respectively, such that the product set of `t₁` and `t₂` is a subset of `s`. In other words, `s` is included in the product filter of `f` and `g` exactly when it includes a product of a set from `f` and a set from `g`.
More concisely: For filters $f$ on type $\alpha$ and $g$ on type $\beta$, the set $s$ of pairs $(a, b): \alpha \times \beta$ is in the product filter of $f$ and $g$ if and only if there exist $A \subseteq \alpha$ in $f$ and $B \subseteq \beta$ in $g$ such that $A \times B \subseteq s$.
|
Filter.prod_principal_principal
theorem Filter.prod_principal_principal :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β},
Filter.principal s ×ˢ Filter.principal t = Filter.principal (s ×ˢ t)
This theorem states that for any two types `α` and `β`, and any two sets `s` of type `α` and `t` of type `β`, the product of the principal filters of `s` and `t` is equal to the principal filter of the product of `s` and `t`. In mathematical terms, given sets `s ⊆ α` and `t ⊆ β`, the principal filter generated by the Cartesian product `s × t` is the same as the Cartesian product of the principal filters generated by `s` and `t` respectively.
More concisely: The principal filters of sets `s ⊆ α` and `t ⊆ β` have the same elements as the principal filter generated by the Cartesian product `s × t`.
|
Filter.Eventually.diag_of_prod
theorem Filter.Eventually.diag_of_prod :
∀ {α : Type u_1} {f : Filter α} {p : α × α → Prop}, (∀ᶠ (i : α × α) in f ×ˢ f, p i) → ∀ᶠ (i : α) in f, p (i, i)
This theorem states that if a property is eventually true for all pairs `l ×ˢ l` drawn from a given filter `f`, then that property is also eventually true for all diagonal pairs `(i, i)` from the same filter. In other words, if a predicate `p` holds for almost all pairs in the product of a filter with itself, then `p` also holds for almost all elements in the filter when considered as pairs with identical first and second elements.
More concisely: If a property holds for almost all pairs in the product of a filter with itself in Lean 4, then it also holds for almost all diagonal pairs from the same filter.
|