Filter.HasBasis.sup
theorem Filter.HasBasis.sup :
∀ {α : Type u_1} {l l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s → l'.HasBasis p' s' → (l ⊔ l').HasBasis (fun i => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2
The theorem `Filter.HasBasis.sup` states that given two filters `l` and `l'` over a Type `α`, indexed by Types `ι` and `ι'` respectively, and if the filter `l` has a basis that satisfies a property `p` and the filter `l'` has a basis that satisfies a property `p'`, then the supremum of `l` and `l'` (denoted `l ⊔ l'`) also has a basis. The basis of the supremum filter is characterized by the conjunction of the properties `p` and `p'` (represented by `(fun i => p i.1 ∧ p' i.2)`) and the union of the sets associated with `l` and `l'` (represented by `(fun i => s i.1 ∪ s' i.2)`). In essence, it describes how the basis properties and sets of the two filters combine when they are merged together.
More concisely: The supremum of two filters over a Type has a basis if and only if the bases of the two filters have the conjunction of their property conditions and the union of their associated sets.
|
Filter.mem_prod_self_iff
theorem Filter.mem_prod_self_iff :
∀ {α : Type u_1} {la : Filter α} {s : Set (α × α)}, s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s
This theorem states that for any type `α`, any filter `la` on `α`, and any set `s` of pairs of `α`, `s` is in the product of `la` with itself if and only if there exists a set `t` in `la` such that the Cartesian product of `t` with itself is a subset of `s`. Here, the Cartesian product `t ×ˢ t` of `t` with itself is the set of all ordered pairs `(a, b)` where `a` and `b` are both elements of `t`. A filter `la` on a type `α` is a particular collection of subsets of `α` that satisfies certain mathematical conditions.
More concisely: For any filter `la` on a type `α` and any set `s` of pairs from `α`, `s` is in the product of `la` with itself if and only if there exists a set `t` in `la` such that `t × t` is a subset of `s`.
|
Filter.IsBasis.inter
theorem Filter.IsBasis.inter :
∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α},
Filter.IsBasis p s → ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j
The theorem `Filter.IsBasis.inter` states that for any type `α` and any index type `ι`, given a predicate `p` on `ι`, and a function `s` from `ι` to sets of `α` such that `p` and `s` form a filter basis, for any `i` and `j` of type `ι` that satisfy the predicate `p`, there exists an `k` of type `ι` such that `p k` is true and the set `s k` is a subset of the intersection of the sets `s i` and `s j`. This theorem is about the property of filter bases where they are directed downwards on indices satisfying a certain property.
More concisely: For any filter basis `(p : ι -> Prop)` and `(s : ι -> Set α)` on a type `α`, if `p` and `s` satisfy the downward closure property such that for any `i` and `j` with `p i` and `p j` and `i ≠ j`, there exists `k` with `p k`, `i ≤ k`, and `s k ⊆ s i ∩ s j`, then for any `i` and `j` with `p i` and `p j`, there exists `k` with `p k` such that `s k` is a subset of the intersection of `s i` and `s j`.
|
Filter.HasBasis.prod
theorem Filter.HasBasis.prod :
∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {pa : ι → Prop}
{sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β},
la.HasBasis pa sa →
lb.HasBasis pb sb → (la ×ˢ lb).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2
This theorem states that for any two types `α` and `β`, two filters `la` and `lb` on these types, two types `ι` and `ι'`, two properties `pa` and `pb` dependent on `ι` and `ι'` respectively, and two set-valued functions `sa` and `sb` dependent on `ι` and `ι'` respectively, if `la` has a basis represented by the property-set pair `(pa, sa)` and `lb` has a basis represented by the property-set pair `(pb, sb)`, then the product filter `(la ×ˢ lb)` has a basis represented by the property-set pair `((fun i => pa i.1 ∧ pb i.2), (fun i => sa i.1 ×ˢ sb i.2))`. In other words, the basis of the product of two filters is constructed from the bases of the individual filters by taking the product of their properties and their associated sets.
More concisely: Given filters `la` and `lb` on types `α` and `β` with property-set basis `(pa, sa)` and `(pb, sb)` respectively, the product filter `la ×ˢ lb` has a basis represented by the property-set `((∧) <$> (pure ∧) <$> [pa, pb], (<*>) <$> sa <*> sb)`.
|
Filter.HasBasis.eq_iInf
theorem Filter.HasBasis.eq_iInf :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {s : ι → Set α},
l.HasBasis (fun x => True) s → l = ⨅ i, Filter.principal (s i)
This theorem states that for any type `α` and an indexing type `ι`, given a filter `l` on `α` and a function `s` from `ι` to the set of `α`, if `l` has a basis such that every set in the basis is included (the predicate is always true), then the filter `l` is equal to the infimum of the principal filters of the sets `s(i)` as `i` varies over `ι`. Here, a principal filter of a set `s` is the collection of all supersets of `s`, and the infimum of a collection of filters is the greatest filter that is less than or equal to all filters in the collection.
More concisely: If `α` is a type, `ι` is an indexing type, `l` is a filter on `α`, `s` is a function from `ι` to `α`, and `l` has a basis consisting of sets all included in some `s(i)`, then `l` is the infimum of the principal filters of `s(i)` as `i` varies over `ι`.
|
Filter.HasBasis.inf_basis_neBot_iff
theorem Filter.HasBasis.inf_basis_neBot_iff :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s →
l'.HasBasis p' s' → ((l ⊓ l').NeBot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty)
The theorem `Filter.HasBasis.inf_basis_neBot_iff` states that for any two types `α` and `ι`, and two sorts `ι'` and `u_5`, given any two filters `l` and `l'` over `α`, any two predicate functions `p : ι → Prop` and `p' : ι' → Prop`, and any two functions `s : ι → Set α` and `s' : ι' → Set α`, if `l` and `l'` are filter bases with respect to these functions, then the intersection of `l` and `l'` is not a bottom element (i.e., is non-empty) if and only if for all `i` in `ι` such that `p i` holds and for all `i'` in `ι'` such that `p' i'` holds, the intersection of the sets `s i` and `s' i'` is non-empty. In other words, two filter bases `l` and `l'` will have a non-empty intersection if and only if the corresponding sets of their valid basis elements also have a non-empty intersection.
More concisely: Two filters over a type have a non-empty intersection as filter bases if and only if the corresponding sets of their valid basis elements intersect non-emptily for all pairs of elements valid under their respective predicate functions.
|
Filter.HasBasis.to_hasBasis'
theorem Filter.HasBasis.to_hasBasis' :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s →
(∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) → (∀ (i' : ι'), p' i' → s' i' ∈ l) → l.HasBasis p' s'
This theorem states that for any type `α`, index types `ι` and `ι'`, a filter `l` on `α`, two predicates `p` and `p'` on `ι` and `ι'` respectively, and two functions `s` and `s'` from `ι` and `ι'` to sets of `α` respectively, if `l` has a basis characterized by `p` and `s`, and for every index `i` of type `ι` for which `p i` holds, there exists an index `i'` of type `ι'` such that `p' i'` holds and `s' i'` is a subset of `s i`, and for every index `i'` of type `ι'` for which `p' i'` holds, `s' i'` belongs to `l`, then `l` also has a basis characterized by `p'` and `s'`. This theorem is about the transferability of basis properties in the context of filters.
More concisely: If a filter on a type has a basis characterized by a predicate and a function, and for each index satisfying the predicate there exists another index with the same property and the function mapping to a subset, and conversely every index satisfying the second predicate is in the filter, then the filter has an equivalent basis given by the second predicate and function.
|
Filter.HasBasis.ge_iff
theorem Filter.HasBasis.ge_iff :
∀ {α : Type u_1} {ι' : Sort u_5} {l l' : Filter α} {p' : ι' → Prop} {s' : ι' → Set α},
l'.HasBasis p' s' → (l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l)
The theorem `Filter.HasBasis.ge_iff` states that for all types `α` and `ι'`, and for all filters `l` and `l'` on `α`, and for all properties `p'` on `ι'` and sets `s'` of `α` indexed by `ι'`, if the filter `l'` has a basis characterized by the property `p'` and the sets `s'`, then the filter `l` is greater than or equal to the filter `l'` if and only if for every `ι'` for which `p'` holds, the corresponding set `s'` is an element of the filter `l`. In simpler terms, it means that one filter is larger than another if it contains every set from the basis of the smaller filter that satisfies a certain property.
More concisely: For filters `l` and `l'` on type `α`, `l ≥ l'` if and only if for every `ι'` such that property `p'` holds for `l'`'s basis set `s'`, `s' ∈ l`.
|
Filter.HasBasis.tendsto_iff
theorem Filter.HasBasis.tendsto_iff :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α}
{lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β},
la.HasBasis pa sa →
lb.HasBasis pb sb → (Filter.Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib)
This theorem, `Filter.HasBasis.tendsto_iff`, states that for any types `α`, `β`, `ι`, `ι'`, any filters `la` on `α` and `lb` on `β`, any properties `pa : ι → Prop` and `pb : ι' → Prop`, any sets `sa : ι → Set α` and `sb : ι' → Set β`, and any function `f : α → β`, if `la` has a basis characterized by `pa` and `sa`, and `lb` has a basis characterized by `pb` and `sb`, then the function `f` tends from `la` to `lb` if and only if for all `ib` such that `pb ib` holds, there exists an `ia` such that `pa ia` holds and for all `x` in the set `sa ia`, `f x` belongs to the set `sb ib`.
In other words, under the given conditions, `f` tends from `la` to `lb` precisely when, for each basis element of `lb` indexed by some `ib` satisfying `pb`, we can find a basis element of `la` indexed by some `ia` satisfying `pa` such that the image under `f` of this basis element is contained in the basis element of `lb`.
More concisely: A function between two filter spaces tends from one filter to another if and only if for every basis element of the target filter indexed by an element satisfying the corresponding property, there exists a basis element of the source filter indexed by an element with the same property such that the image of the source basis element is contained in the target basis element.
|
Filter.exists_antitone_basis
theorem Filter.exists_antitone_basis :
∀ {α : Type u_1} (f : Filter α) [inst : f.IsCountablyGenerated], ∃ x, f.HasAntitoneBasis x
This theorem states that for any countably generated filter `f` over a type `α`, there exists a sequence `x` such that `x` forms an antitone basis for the filter `f`. In other words, if a filter is generated by countably many sets, it's possible to find a sequence of sets that descends (each set is contained in the ones before it) and can serve as a base for the filter.
More concisely: For any countably generated filter on a type, there exists a countable antichain that generates the filter.
|
Filter.hasBasis_biInf_principal'
theorem Filter.hasBasis_biInf_principal' :
∀ {α : Type u_1} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α},
(∀ (i : ι), p i → ∀ (j : ι), p j → ∃ k, p k ∧ s k ⊆ s i ∧ s k ⊆ s j) →
(∃ i, p i) → (⨅ i, ⨅ (_ : p i), Filter.principal (s i)).HasBasis p s
This theorem states that, for any type `α` and index type `ι`, given a predicate `p : ι → Prop` and a function `s : ι → Set α` such that for every pair of indices `i` and `j` for which `p` holds, there exists an index `k` for which `p` also holds and the sets `s k` are subsets of both `s i` and `s j`, and there exists at least one index for which `p` holds, then the Filter generated by the infimum over all i of the principal filters of `s i` for which `p i` holds, has a basis characterized by the predicate `p` and the function `s`. In other words, we have a filter basis formed by sets `s i` for the indices `i` for which the predicate `p` is true.
More concisely: Given a type `α`, an index type `ι`, a predicate `p : ι → Prop`, and a function `s : ι → Set α` such that for any pair `i`, `j` with `p i` and `p j` holding and `s i ⊆ s k` and `s j ⊆ s k` for some `k`, there exists an index with `p` holding having this property, and there exists at least one index with `p` holding: the filter basis of the infimum of the principal filters of `s i` for `i` with `p i` is `p` and `s`.
|
FilterBasis.mem_filter_of_mem
theorem FilterBasis.mem_filter_of_mem : ∀ {α : Type u_1} (B : FilterBasis α) {U : Set α}, U ∈ B → U ∈ B.filter := by
sorry
The theorem `FilterBasis.mem_filter_of_mem` states that for any type `α`, given a filter basis `B` of this type and a set `U` of the same type, if the set `U` is an element of the filter basis `B`, then `U` is also an element of the filter associated with the filter basis `B`. This essentially says that any set that belongs to a filter basis will automatically belong to the filter generated by that basis.
More concisely: If `B` is a filter basis for the type `α`, and `U` is an element of `B`, then `U` is a member of the filter `filterBASIS B`.
|
Filter.HasBasis.neBot_iff
theorem Filter.HasBasis.neBot_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → (l.NeBot ↔ ∀ {i : ι}, p i → (s i).Nonempty)
This theorem states that for any type `α`, any sort `ι`, any filter `l` of `α`, and any properties `p` and sets `s` indexed by `ι`, if the filter `l` has a filter basis given by the properties `p` and sets `s`, then the filter `l` is not a bottom filter if and only if for every index `i` of sort `ι` for which the property `p i` holds, the corresponding set `s i` is nonempty. In other words, the filter is nonempty if every set in its basis that satisfies a certain condition is also nonempty.
More concisely: For any filter `l` over type `α` with basis given by properties `p` and sets `s` indexed by sort `ι`, `l` is not a bottom filter if and only if for all `i` in `ι` where `p i` holds, `s i` is nonempty.
|
Filter.IsAntitoneBasis.antitone
theorem Filter.IsAntitoneBasis.antitone :
∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {s'' : ι'' → Set α},
Filter.IsAntitoneBasis s'' → Antitone s''
The theorem `Filter.IsAntitoneBasis.antitone` states that if we have a sequence of sets `s''` indexed by a type `ι''` which has a preorder structure, and if this sequence forms an antitone basis (i.e., is a basis for a certain filter and satisfies the condition that for any pair of indices `i` and `j`, if `i ≤ j` then `s'' j` is a subset of `s'' i`), then the sequence `s''` itself is antitone, meaning that for any pair of indices `i` and `j`, if `i ≤ j` then `s'' j` is a subset of `s'' i`. This is a claim about the relationship between the structure of a sequence of sets and its ordering.
More concisely: If `s''` is an antitone basis of a filter on a preorder `ι''`, then `s''` is an antitone sequence (i.e., for all `i ≤ j`, `s'' j` is a subset of `s'' i`).
|
Filter.isCountablyGenerated_seq
theorem Filter.isCountablyGenerated_seq :
∀ {α : Type u_1} {ι' : Sort u_5} [inst : Countable ι'] (x : ι' → Set α),
(⨅ i, Filter.principal (x i)).IsCountablyGenerated
This theorem states that for any type `α`, any countable index type `ι'` and any sequence `x` of sets of type `α` indexed by `ι'`, the filter generated by the principle filter on each of the sets `x i` (the infimum over all `i` of the principle filter of `x i`) is countably generated. A filter is countably generated if there exists a countable collection of sets such that the filter is the smallest filter containing that collection.
More concisely: For any countable index type `ι` and countable sequence `(F_i : Filter α)_i` of filters on a type `α`, the filter generated by their principal filters `(principal_filter F_i)_i` is countably generated.
|
Filter.hasBasis_self
theorem Filter.hasBasis_self :
∀ {α : Type u_1} {l : Filter α} {P : Set α → Prop},
l.HasBasis (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
This theorem, `Filter.hasBasis_self`, states that for any type `α`, any filter `l` on `α`, and any property `P` of subsets of `α`, the filter `l` has a basis given by the subsets `s` of `α` that are in `l` and satisfy `P`, using the identity function as the index function, if and only if for all subsets `t` in `l`, there exists a subset `r` in `l` that satisfies `P` and is a subset of `t`. In other words, it provides a characterization of a filter having a basis in terms of the existence of certain subsets satisfying a given property within the filter.
More concisely: A filter on a type has a basis consisting of sets satisfying a given property if and only if every element in the filter contains some other element in the filter that also satisfies the property.
|
Filter.disjoint_principal_left
theorem Filter.disjoint_principal_left :
∀ {α : Type u_1} {f : Filter α} {s : Set α}, Disjoint (Filter.principal s) f ↔ sᶜ ∈ f
This theorem states that for any type `α`, any filter `f` on `α`, and any set `s` of `α`, the principal filter of `s` is disjoint from `f` if and only if the complement of `s` is in `f`. In other words, the principal filter (which is the collection of all supersets of `s`) and `f` do not have any element in common iff the set of all elements not in `s` belongs to the filter `f`. Here, `Disjoint` refers to the concept in lattice theory where two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice.
More concisely: For any filter `f` on type `α` and set `s` of `α`, the principal filter of `s` and `f` are disjoint if and only if the complement of `s` is in `f`.
|
Filter.HasBasis.disjoint_iff_left
theorem Filter.HasBasis.disjoint_iff_left :
∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → (Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l')
This theorem states that for any types `α` and `ι`, along with two filters `l` and `l'` on `α`, a predicate `p : ι → Prop` and a function `s : ι → Set α` that gives a set for each `ι`, if `l` has a basis defined by `p` and `s`, then `l` and `l'` are disjoint if and only if there exists some `i` such that `p i` is true and the complement of `s i` is in `l'`. In other words, the filters `l` and `l'` are disjoint if there exists an `i` satisfying `p` such that all elements not in the set `s i` are in `l'`. This theorem allows us to characterize the disjointness of two filters in terms of the basis of one of them.
More concisely: For filters $l$ and $l'$ on type $\alpha$, if $l$ has basis given by predicate $p$ and function $s$, then $l$ and $l'$ are disjoint if and only if there exists an $i$ such that $p(i)$ holds and the complement of $s(i)$ is contained in $l'$.
|
Filter.HasCountableBasis.countable
theorem Filter.HasCountableBasis.countable :
∀ {α : Type u_1} {ι : Type u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasCountableBasis p s → (setOf p).Countable
This theorem states that for any types `α` and `ι`, any filter `l` of type `α`, any predicate `p` of type `ι → Prop`, and any function `s` from `ι` to a set of `α`, if the filter `l` has a countable basis with respect to the predicate `p` and the function `s`, then the set of elements `i` of type `ι` that satisfy the predicate `p` is countable. In mathematical terms, given a basis for a filter that is countable, the set of indices that satisfy a certain condition (defined by the predicate `p`) is also countable.
More concisely: If a filter on a type has a countable basis with respect to a predicate and a function, then the set of elements satisfying the predicate is countable.
|
Filter.mem_iff_inf_principal_compl
theorem Filter.mem_iff_inf_principal_compl :
∀ {α : Type u_1} {f : Filter α} {s : Set α}, s ∈ f ↔ f ⊓ Filter.principal sᶜ = ⊥
The theorem `Filter.mem_iff_inf_principal_compl` states that for any type `α`, any filter `f` on `α`, and any set `s` of type `α`, the set `s` is a member of the filter `f` if and only if the infimum (greatest lower bound) of the filter `f` and the principal filter of the complement of `s` is the bottom element (`⊥`). In other words, `s` belongs to the filter `f` exactly when there are no elements that belong to both `f` and the principal filter of all sets that do not contain `s`.
More concisely: For any filter `f` on type `α` and set `s` of type `α`, `s` belongs to `f` if and only if the infimum of `f` and the complement of `s`'s principal filter is the bottom element.
|
Filter.HasBasis.mem_of_mem
theorem Filter.HasBasis.mem_of_mem :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {i : ι},
l.HasBasis p s → p i → s i ∈ l
This theorem states that for any types `α` and `ι`, a filter `l` on `α`, a property `p` on `ι`, a function `s` that maps `ι` to a set of `α`, and an element `i` of `ι`, if the filter `l` has a basis given by the property `p` and the function `s`, and the property `p` holds for the element `i`, then the set `s i` is a member of the filter `l`.
In simpler terms, it says that if a filter is defined by certain properties and sets, and if an element satisfies a property, then the corresponding set is part of the filter.
More concisely: If a filter on a type `α` has property `p` as its basis along with function `s` mapping elements of `ι` to `α`, then for any `i` in `ι` satisfying property `p`, we have `s i` in the filter.
|
Filter.HasBasis.eq_bot_iff
theorem Filter.HasBasis.eq_bot_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → (l = ⊥ ↔ ∃ i, p i ∧ s i = ∅)
This theorem states that for any type `α` and an index type `ι`, given a filter `l` over `α`, a predicate `p` over `ι`, and a function `s` from `ι` to sets of `α` such that `l` has a filter basis characterized by `p` and `s`, then `l` is the bottom filter if and only if there exists an index `i` such that `p i` is true and the set `s i` is empty. In the context of filters, the bottom filter essentially represents the "smallest" or "trivial" filter, and filter basis is a method of specifying a filter using a collection of sets that satisfy certain properties.
More concisely: For a filter `l` over type `α` with filter basis characterized by predicate `p` and function `s` from index type `ι` to sets of `α`, `l` is the bottom filter if and only if there exists an index `i` such that `p i` holds and `s i` is empty.
|
Filter.HasBasis.mem_iff'
theorem Filter.HasBasis.mem_iff' :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
The theorem `Filter.HasBasis.mem_iff'` states that for any type `α`, index type `ι`, filter `l` on `α`, predicates `p` on `ι`, and mapping `s` from `ι` to sets on `α`, if the filter `l` has a basis specified by the predicates `p` and the mapping `s`, then a set `t` belongs to the filter `l` if and only if there exists an index `i` such that `p i` holds and the set `s i` is a subset of `t`.
More concisely: For any filter `l` on type `α` with basis given by predicates `p` on index type `ι` and mapping `s` from `ι` to sets on `α`, a set `t` belongs to `l` if and only if there exists an index `i` such that `p i` holds and `s i ⊆ t`.
|
Filter.HasBasis.to_hasBasis
theorem Filter.HasBasis.to_hasBasis :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s →
(∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) →
(∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') → l.HasBasis p' s'
This theorem states that given a filter `l` on a type `α` that has a basis characterized by a predicate `p` on an indexing type `ι` and a mapping `s` from `ι` to sets of `α`, if for every element `i` of `ι` satisfying `p`, there exists an element `i'` satisfying a predicate `p'` on another indexing type `ι'` such that the set `s'(i')` is a subset of `s(i)`, and for every element `i'` of `ι'` satisfying `p'`, there exists an element `i` satisfying `p` such that the set `s(i)` is a subset of `s'(i')`, then `l` also has a basis characterized by the predicate `p'` and the mapping `s'`. This theorem essentially provides a necessary and sufficient condition for a filter to have a certain basis.
More concisely: If a filter on a type has a basis characterized by a predicate and a mapping to sets, and there exists a dual mapping and predicate such that each element in the original indexing type satisfies the predicate if and only if there exists an element in the dual indexing type satisfying the dual predicate with a subset relation between their corresponding sets, then the filter has an equivalent basis characterized by the dual predicate and mapping.
|
Filter.HasBasis.tendsto_right_iff
theorem Filter.HasBasis.tendsto_right_iff :
∀ {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β}
{f : α → β}, lb.HasBasis pb sb → (Filter.Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i)
The theorem `Filter.HasBasis.tendsto_right_iff` states that for any types `α` and `β`, any type of indexing `ι'`, any filter on `α` denoted by `la`, any filter on `β` denoted by `lb`, any property `pb` indexed by `ι'`, any set `sb` of `β` indexed by `ι'`, and any function `f` from `α` to `β`, if `lb` has a basis described by the property `pb` and the corresponding sets `sb`, then the function `f` tends towards the filter `lb` from `la` if and only if for every index `i` of type `ι'` where the property `pb` holds, almost all elements `x` from `α` in the filter `la` satisfy the condition that `f(x)` belongs to the set `sb` at index `i`.
In more mathematical terms, this theorem provides a characterization for the convergence of a function towards a particular filter in terms of the basis of that filter.
More concisely: A function from a filter to another filter converges to the second filter from the first if and only if almost all elements in the first filter map to elements in the corresponding sets of the basis of the second filter.
|
Filter.HasBasis.ker
theorem Filter.HasBasis.ker :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → l.ker = ⋂ i, ⋂ (_ : p i), s i
For any type `α` and index type `ι`, this theorem states that given a filter `l` on the type `α`, a predicate `p` on the index type `ι`, and a function `s` mapping each index to a set of `α`, if this system has a filter basis, then the kernel (i.e., the intersection of all sets) of the filter `l` is the intersection over all indices `i` such that `p i` holds, of the sets `s i`. In simpler terms, the theorem is saying that the kernel of a filter, given a filter basis, can be described as the intersection of certain associated sets, as dictated by the basis.
More concisely: Given a filter `l` on type `α` with filter basis `{s i | ι : Type, i : ι, p i}`, the kernel of `l` equals the intersection over all `i` such that `p i` holds, of the sets `s i`.
|
Filter.HasBasis.prod_self
theorem Filter.HasBasis.prod_self :
∀ {α : Type u_1} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α},
la.HasBasis pa sa → (la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i
The theorem `Filter.HasBasis.prod_self` states that for any type `α` and any sort `ι`, given a filter `la` on `α`, a predicate `pa` on `ι`, and a function `sa` mapping `ι` to a set of elements of type `α`, if `la` has a basis characterized by the predicate `pa` and the set function `sa`, then the product filter (i.e., `la ×ˢ la`) also has a basis characterized by the same predicate `pa` and the set function that maps `ι` to the product set (i.e., `sa i ×ˢ sa i`). Essentially, this theorem says that the basis of a product filter is the product of the bases of the original filters.
More concisely: If filters `la` on type `α` and `lb` on sort `ι` have bases characterized by predicate `pa` and set functions `sa` and `sb` respectively, then the product filter `la ×ˢ lb` has a basis characterized by predicate `pa` and the set function mapping `ι` to `sa i ×ˢ sb i`.
|
Mathlib.Order.Filter.Bases._auxLemma.4
theorem Mathlib.Order.Filter.Bases._auxLemma.4 : ∀ {α : Type u} {s t : Set α}, (s ∈ Filter.principal t) = (t ⊆ s) := by
sorry
This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, `s` is in the principal filter of `t` if and only if `t` is a subset of `s`. In other words, a set `s` is a part of the collection of all supersets of another set `t` (the principal filter of `t`) precisely when every element of `t` is also an element of `s`.
More concisely: For any type `α` and sets `s` and `t` of type `α`, `s` is the principal filter of `t` if and only if `t` is a subset of `s`.
|
Filter.HasBasis.frequently_iff
theorem Filter.HasBasis.frequently_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → ∀ {q : α → Prop}, (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
This theorem states that for any type `α` and indexing type `ι`, given a filter `l` on `α`, a predicate `p` on `ι`, and a function `s` mapping `ι` to sets of `α` such that `l` has the basis `p` and `s`, for any predicate `q` on `α`, the event "there exist frequently `x` in `l` such that `q x` is true" is equivalent to "for any index `i` in `ι` for which `p i` is true, there exists an element `x` in the set `s i` such that `q x` is true".
Here, "frequently" means the event occurs in `l` on a set of indices with full measure. The term "basis for a filter" refers to a collection of sets that can be used to generate the filter, and it satisfies certain properties like any element of the basis intersects with some other element of the basis.
More concisely: Given a filter `l` on type `α` with basis `{p : ι → Prop, s : ι → set α | p ∧ l.is_closed p ∧ ∀ i, p i → ∃ x ∈ s i, q x}`, the event "there exists an x in l with q(x) true" is equivalent to "for all i in ι with p(i), there exists an x in s(i) with q(x) true".
|
Filter.HasBasis.eq_biInf
theorem Filter.HasBasis.eq_biInf :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → l = ⨅ i, ⨅ (_ : p i), Filter.principal (s i)
The theorem `Filter.HasBasis.eq_biInf` states that for any type `α`, any sort `ι`, any Filter `l` on `α`, any predicate `p` on `ι`, and any function `s` from `ι` to a set of `α`, if `l` has a filter basis determined by the predicate `p` and the function `s`, then `l` is equal to the infimum of the principal filters of the sets `s i`, for each `i` that satisfies the predicate `p`. This infimum is taken twice, once over `i` and once over those `i` that satisfy `p`. In other words, `l` is characterized by the smallest filters that contain all sets `s i` for `i` meeting the condition `p i`.
More concisely: For any type `α`, Filter `l` on `α`, predicate `p` on a sort `ι`, and function `s` from `ι` to `α`, if `l` is the infimum of the principal filters of `{s i | i ∈ ι & p i}`, then `l` has a filter basis determined by `p` and `s`.
|
Filter.HasCountableBasis.isCountablyGenerated
theorem Filter.HasCountableBasis.isCountablyGenerated :
∀ {α : Type u_1} {ι : Type u_4} {f : Filter α} {p : ι → Prop} {s : ι → Set α},
f.HasCountableBasis p s → f.IsCountablyGenerated
This theorem states that for any type `α` and `ι`, and for any filter `f` of the type `α` and predicate `p` and function `s` from `ι` to the set of `α`, if the filter `f` has a countable basis defined by predicate `p` and function `s`, then the filter `f` is countably generated. Here, a countable basis of a filter means a countable collection of sets that the filter is built from, and a countably generated filter means a filter that is generated from a countable collection of sets.
More concisely: If a filter on type `α` has a countable basis defined by a predicate and a function from a countable type, then the filter is countably generated.
|
Filter.HasBasis.forall_iff
theorem Filter.HasBasis.forall_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s →
∀ {P : Set α → Prop}, (∀ ⦃s t : Set α⦄, s ⊆ t → P s → P t) → ((∀ s ∈ l, P s) ↔ ∀ (i : ι), p i → P (s i))
This theorem states that for a given type `α` and a filter `l` on `α`, if the filter has a basis characterized by a predicate `p` on an index type `ι` and a map `s` from `ι` to the set of `α`, then for any property `P` which holds for subsets of a set if it holds for that set, it holds for all sets in the filter if and only if it holds for all sets in the basis where the predicate `p` is true. In other words, the filter satisfies a property for all its sets if and only if its basis sets satisfying the predicate also satisfy this property.
More concisely: Given a filter `l` on type `α` with basis characterized by predicate `p` on index type `ι` and map `s`, if property `P` holds for sets if and only if it holds for sets in the basis where `p` is true, then `P` holds for all sets in the filter if and only if it holds for all sets in the basis.
|
Filter.isCountablyGenerated_of_seq
theorem Filter.isCountablyGenerated_of_seq :
∀ {α : Type u_1} {f : Filter α}, (∃ x, f = ⨅ i, Filter.principal (x i)) → f.IsCountablyGenerated
The theorem `Filter.isCountablyGenerated_of_seq` states that for any type `α` and any filter `f` on this type, if there exists a sequence `x` such that the filter `f` is the infimum over all filters generated by the principal filter of the sequence `x`, then `f` is countably generated. In simpler terms, if a filter is the intersection of countably many filters, each generated by a set, then it's a countably generated filter.
More concisely: If a filter on a type is the intersection of countably many principal filters, then it is countably generated.
|
Filter.hasBasis_principal
theorem Filter.hasBasis_principal :
∀ {α : Type u_1} (t : Set α), (Filter.principal t).HasBasis (fun x => True) fun x => t
The theorem `Filter.hasBasis_principal` states that for any type `α` and any set `t` of that type, the principal filter of `t` has a basis that consists of the set `t` itself. Here, a filter's basis is a collection of sets such that any set in the filter can be written as a union of sets in the basis. In more informal terms, this theorem says that the principal filter of any set can be fully understood by considering the set itself; all other sets in the filter are just supersets of the original set.
More concisely: The principal filter of a set has that set itself as a basis.
|
Filter.HasBasis.mem_iff
theorem Filter.HasBasis.mem_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α},
l.HasBasis p s → (t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t)
The theorem `Filter.HasBasis.mem_iff` provides a condition for the membership of a set `t` in a filter `l`. This condition is based on the concept of a basis of a filter. For any types `α` and `ι`, a filter `l` on `α`, a property `p` of `ι`, and a function `s` from `ι` to the set of `α`, the theorem states that if the filter `l` has a basis characterized by `p` and `s`, then the set `t` is in the filter `l` if and only if there exists an `i` such that `p i` holds and the set `s i` is a subset of `t`.
More concisely: A set `t` belongs to a filter `l` with basis `(p : ∀ i, Prop ι)` and `s : ∀ i, α → α` if and only if there exists an `i` such that `p i` holds and `s i ⊆ t`.
|
Filter.CountableFilterBasis.countable
theorem Filter.CountableFilterBasis.countable :
∀ {α : Type u_6} (self : Filter.CountableFilterBasis α), self.sets.Countable
This theorem states that for any given countable filter basis (a concept from the field of topology) of a particular type 'α', the set of all sets within this filter basis is also countable. In other words, we can enumerate all the sets in the filter basis in a sequence (a countable sequence).
More concisely: A countable filter basis of a set 'α' is a countable collection of sets.
|
FilterBasis.generate
theorem FilterBasis.generate : ∀ {α : Type u_1} (B : FilterBasis α), Filter.generate B.sets = B.filter
This theorem states that for any given filter basis `B` of a type `α`, the filter generated by the sets of `B` (`Filter.generate B.sets`) is equivalent to the filter associated with the filter basis `B` (`FilterBasis.filter B`). In other words, generating a filter from the sets of a filter basis gives you the same result as directly associating a filter with the filter basis.
More concisely: For any filter basis `B` of type `α`, `Filter.generate B.sets` is equivalent to `FilterBasis.filter B`.
|
Mathlib.Order.Filter.Bases._auxLemma.10
theorem Mathlib.Order.Filter.Bases._auxLemma.10 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = (a ∧ b ∧ c)
This theorem, `Mathlib.Order.Filter.Bases._auxLemma.10`, states that for any three propositions `a`, `b`, and `c`, the proposition "`a` and `b` and `c`" is logically equivalent to the proposition "(`a` and `b`) and `c`". In other words, the conjunction (and-operation) is associative in propositional logic.
More concisely: The theorem `Mathlib.Order.Filter.Bases._auxLemma.10` in Lean 4 states that the conjunction of three propositions `a`, `b`, and `c` is logically equivalent to the conjunction of `a` and `b` with `c`. In mathematical notation, `(a ∧ b) ∧ c` is equivalent to `a ∧ b ∧ c`.
|
Filter.HasAntitoneBasis.antitone
theorem Filter.HasAntitoneBasis.antitone :
∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
l.HasAntitoneBasis s → Antitone s
This theorem states that for any type `α` and any preordered type `ι''`, given a filter `l` on `α` and a function `s` from `ι''` to the set of `α`, if the filter `l` has an antitone basis determined by the function `s`, then the function `s` itself is antitone. In other words, if `a ≤ b` in the preordered set `ι''`, then the set `s(b)` is a subset of or equal to the set `s(a)`.
More concisely: If a filter on a type `α` has an antitone basis given by a function `s` from a preordered type `ι''`, then `s` is an antitone function. That is, for all `a ≤ b` in `ι''`, we have `s(a) ⊇ s(b)`.
|
Filter.HasBasis.map
theorem Filter.HasBasis.map :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : α → β),
l.HasBasis p s → (Filter.map f l).HasBasis p fun i => f '' s i
The theorem `Filter.HasBasis.map` states that for any types `α`, `β` and a sort `ι`, given a filter `l` on `α`, a property `p` on `ι`, a map `s` from `ι` to a set of `α`, and a function `f` from `α` to `β`, if `l` has a filter basis determined by the property `p` and the map `s`, then the mapped filter `Filter.map f l` also has a filter basis determined by the same property `p` and the image under `f` of the sets produced by `s`. In simpler terms, the theorem asserts that filter bases are preserved under function mapping.
More concisely: Given a filter `l` on type `α`, property `p` on type `ι`, map `s` from `ι` to `α`, and function `f` from `α` to `β`, if `l` has a filter basis determined by `p` and `s`, then `Filter.map f l` also has a filter basis determined by `p` and the image of `s` under `f`.
|
Filter.IsCountablyGenerated.out
theorem Filter.IsCountablyGenerated.out :
∀ {α : Type u_1} {f : Filter α} [self : f.IsCountablyGenerated], ∃ s, s.Countable ∧ f = Filter.generate s := by
sorry
This theorem states that for any filter `f` on a type `α`, if `f` is countably generated (as indicated by the typeclass assumption `self : f.IsCountablyGenerated`), then there exists a countable set `s` that generates the filter `f`. In other words, the filter `f` can be constructed from the set `s` using the `Filter.generate` function and `s` is a countable set.
More concisely: For any countably generated filter `f` on type `α` in Lean 4, there exists a countable set `s` that generates `f`.
|
Filter.HasBasis.comap
theorem Filter.HasBasis.comap :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : β → α),
l.HasBasis p s → (Filter.comap f l).HasBasis p fun i => f ⁻¹' s i
The theorem `Filter.HasBasis.comap` states that for every pair of types `α` and `β`, a sort `ι`, a filter `l` on `α`, a function `p` from `ι` to `Prop`, and a function `s` from `ι` to a set of `α`, along with a function `f` from `β` to `α`, if we have a basis for the filter `l` defined by the predicates `p` and the sets `s`, then we also have a basis for the filter obtained by the function `f` composed with `l`, where the basis is defined by the predicates `p` and the preimage of the sets `s` under the function `f`.
More concisely: If `l` is a filter on `α` with basis `{p : ι → Prop, s : ι → set α | ∀ i, ∃ x : α, p i ∧ l x = s i}`, then `f '' l` has basis `{p, ∥f∥ '' s}`, where `∥f∥` is the function mapping a set to its image under `f`.
|
Filter.HasBasis.restrict_subset
theorem Filter.HasBasis.restrict_subset :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → ∀ {V : Set α}, V ∈ l → l.HasBasis (fun i => p i ∧ s i ⊆ V) s
The theorem `Filter.HasBasis.restrict_subset` states that for any type `α`, index type `ι`, filter `l` on `α`, predicate `p` on `ι`, and function `s` from `ι` to set of `α`, if `{s i | p i}` forms a basis of the filter `l` and a set `V` is in the filter `l`, then the collection `{s i | p i ∧ s i is a subset of V}` also forms a basis of the filter `l`. Essentially, we can restrict the basis of the filter to the subsets of `V` that also satisfy the predicate `p`.
More concisely: If a collection of subsets of a filter forms a basis and is contained in a given set, then the restriction of that collection to the subsets in the set also forms a basis for the filter.
|
Filter.HasBasis.eventually_iff
theorem Filter.HasBasis.eventually_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → ∀ {q : α → Prop}, (∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x
The theorem `Filter.HasBasis.eventually_iff` states that for any type `α`, a filter `l`, and a function `s` mapping type `ι` to a set of `α`, if `l` has a basis that satisfies property `p` and is given by `s`, then for any predicate `q` on `α`, the statement "eventually in `l`, `q` holds for `x`" is equivalent to: there exists an `i` such that `i` satisfies `p` and for all `x` in the set `s i`, `q x` holds. In other words, the property `q` holds eventually in `l` if and only if there is an index from the basis of `l` whose corresponding set has all its elements satisfying `q`.
More concisely: A filter on a type has a basis satisfying property p if and only if for every predicate q, eventual membership in the filter under p is equivalent to belonging to some set in the basis of the filter where q holds for all elements.
|
Filter.HasBasis.le_basis_iff
theorem Filter.HasBasis.le_basis_iff :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α}, l.HasBasis p s → l'.HasBasis p' s' → (l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i')
This theorem states that for any two types `α` and `ι` along with their variants `ι'`, and given two filters `l` and `l'` on the type `α`, along with two properties `p : ι → Prop` and `p' : ι' → Prop` and two functions `s : ι → Set α` and `s' : ι' → Set α` that map each index to a set of elements of type `α`, if `l` and `l'` have the bases defined by `p`, `s` and `p'`, `s'` respectively, then `l` is less than or equal to `l'` (in the sense of filter inclusion) if and only if for every index `i'` where `p' i'` holds, there exists an index `i` such that `p i` holds and the set `s i` is a subset of `s' i'`.
More concisely: For filters `l` and `l'` on types `α` with index types `ι` and `ι'`, and functions `s` and `s'` mapping indices to sets of elements in `α`, if `l` is defined by properties `p : ι → Prop` and `s : ι → Set α`, and `l'` is defined by `p' : ι' → Prop` and `s' : ι' → Set α`, then `l` is a subset of `l'` if and only if for all `i'` such that `p' i'` holds, there exists an `i` with `p i` holding and `s i` a subset of `s' i'`.
|
Filter.HasBasis.exists_iff
theorem Filter.HasBasis.exists_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s →
∀ {P : Set α → Prop}, (∀ ⦃s t : Set α⦄, s ⊆ t → P t → P s) → ((∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i))
The theorem `Filter.HasBasis.exists_iff` states that for any type `α`, any type of sorting `ι`, any filter `l` of type `α`, any property `p` of `ι`, and any function `s` from `ι` to a set of `α`, if `l` has a basis given by `p` and `s`, then for any property `P` of a set of `α` that is preserved under taking subsets, there exists a set `s` in `l` such that `P` holds for `s` if and only if there exists an index `i` such that `p` holds for `i` and `P` holds for `s(i)`.
In other words, it translates the existence of a certain property in a filter to an equivalent formulation in terms of its basis.
More concisely: For any filter `l` on type `α`, property `p` of indices, and set-preserving property `P` on subsets of `α`, if `l` has basis `s` given by `p`, then `P` holds for some element in `l` if and only if there exists an index `i` such that both `p(i)` holds and `P(s(i))` holds.
|
Disjoint.filter_principal
theorem Disjoint.filter_principal :
∀ {α : Type u_1} {s t : Set α}, Disjoint s t → Disjoint (Filter.principal s) (Filter.principal t)
This theorem, known as `Disjoint.filter_principal`, states that for any given type `α` and any two sets `s` and `t` of this type, if `s` and `t` are disjoint sets (meaning their intersection, or `inf`, is the bottom element), then their principal filters are also disjoint. Simply put, the concept of disjointness is preserved under the operation of forming principal filters.
More concisely: If sets `s` and `t` of type `α` are disjoint, then their principal filters `filter.at_top s` and `filter.at_top t` are also disjoint.
|
Filter.HasBasis.inf
theorem Filter.HasBasis.inf :
∀ {α : Type u_1} {l l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s → l'.HasBasis p' s' → (l ⊓ l').HasBasis (fun i => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2
The theorem `Filter.HasBasis.inf` states that for any two filters `l` and `l'` on a type `α`, indexed over types `ι` and `ι'` respectively, with associated properties `p` and `p'` and sets `s` and `s'`, if `l` has a basis characterized by property `p` and associated sets `s`, and `l'` has a basis characterized by property `p'` and associated sets `s'`, then the intersection of the filters `l` and `l'` also has a basis. The basis of the intersection filter is characterized by the properties `p` and `p'` both holding, and the sets are the intersections of the corresponding sets in the bases of `l` and `l'.
More concisely: If filters `l` and `l'` on type `α` have bases characterized by properties `p` and `p'` and sets `s` and `s'` respectively, then their intersection has a basis with properties `p ∧ p'` and sets `s ∩ s'`.
|
Filter.HasBasis.ex_mem
theorem Filter.HasBasis.ex_mem :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α}, l.HasBasis p s → ∃ i, p i
The theorem `Filter.HasBasis.ex_mem` states that for any type `α`, any type `ι`, any filter `l` on `α`, and any functions `p` from `ι` to `Prop` and `s` from `ι` to `Set α`, if the filter `l` has a basis characterized by the properties `p` and sets `s`, then there exists an `i` such that the property `p` holds true for `i`.
In other words, if a filter has a basis, then there exists at least one element in this basis that satisfies a certain property.
More concisely: If a filter on a type has a basis characterized by a property and sets, then there exists an element in the basis with the property.
|
Filter.HasBasis.inf_principal
theorem Filter.HasBasis.inf_principal :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → ∀ (s' : Set α), (l ⊓ Filter.principal s').HasBasis p fun i => s i ∩ s'
This theorem states that for any type `α`, any indexing type `ι`, any filter `l` on `α`, any predicate `p` on `ι`, any function `s` from `ι` to a set of `α`, and any given set `s'` of `α`, if the filter `l` has a basis characterized by the predicate `p` and the function `s`, then the intersection of the filter `l` and the principal filter of `s'` (that is, the filter containing all supersets of `s'`) has a basis characterized by the predicate `p` and the function that maps `i` to the intersection of `s i` and `s'`. In simpler terms, the basis of a filter and the basis of its intersection with a principal filter are closely related.
More concisely: If filters `l` and `m` have bases characterized by predicate `p` and functions `s` and `t` respectively, then the intersection `l ∩ ℙ(s')` has a basis characterized by predicate `p` and the function `x ↦ s x ∩ s'`.
|
Filter.HasBasis.restrict
theorem Filter.HasBasis.restrict :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s →
∀ {q : ι → Prop}, (∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i) → l.HasBasis (fun i => p i ∧ q i) s
This theorem states that, given a filter `l` on some type `α`, indexed by a type `ι`, if `{s i | p i}` forms a basis of this filter and for every `i` such that `p i` is true, there exists a `j` such that both `p j` and `q j` are true and the set `s j` is a subset of `s i`, then the collection `{s j | p j ∧ q j}` also forms a basis of filter `l`. In simpler terms, if a filter has a basis where every element includes another set fulfilling some additional property, then the filter also has a basis composed of those included sets.
More concisely: If `{s i | p i}` is a basis for a filter `l` on type `α` indexed by `ι`, and for all `i`, if `p i` holds then there exists a `j` such that `p j` and `q j` hold and `s j` is a subset of `s i`, then `{s j | p j ∧ q j}` is also a basis for filter `l`.
|
Filter.hasBasis_iInf_principal_finite
theorem Filter.hasBasis_iInf_principal_finite :
∀ {α : Type u_1} {ι : Type u_6} (s : ι → Set α),
(⨅ i, Filter.principal (s i)).HasBasis (fun t => t.Finite) fun t => ⋂ i ∈ t, s i
The theorem `Filter.hasBasis_iInf_principal_finite` states that for any type `α` and index type `ι`, given an indexed family of sets `s : ι → Set α`, the finite intersections of sets in the family `s i` form a basis for the infimum of the principal filters of the sets `s i`. In other words, the basis of the infimum of these principal filters is comprised of the finite intersections of the sets in the indexed family.
More concisely: For any indexed family of sets `s : ι → Set α`, the finite intersections of sets in `s` form a basis for the infimum of their principal filters.
|
FilterBasis.inter_sets
theorem FilterBasis.inter_sets :
∀ {α : Type u_6} (self : FilterBasis α) {x y : Set α}, x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
The theorem `FilterBasis.inter_sets` states that for any type 'α' and any given filter basis 'self' of that type, if 'x' and 'y' are sets belonging to this filter basis, then there exists another set 'z' within the filter basis such that 'z' is a subset of the intersection of 'x' and 'y'. Essentially, the set of filter basis sets is directed downwards, meaning that for any two sets in the filter basis, there is a third set in the filter basis that is contained within the intersection of the first two sets.
More concisely: For any filter basis 'self' of type 'α', if 'x' and 'y' are sets in 'self', then there exists a set 'z' in 'self' such that 'z' is a subset of both 'x' and 'y'.
|
Filter.HasBasis.disjoint_iff
theorem Filter.HasBasis.disjoint_iff :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s → l'.HasBasis p' s' → (Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i'))
This theorem states that for any types `α`, `ι` and `ι'`, any filters `l` and `l'` on `α`, and any functions `p : ι → Prop`, `s : ι → Set α`, `p' : ι' → Prop` and `s' : ι' → Set α`, if `l` has a basis indexed by `ι` with index property `p` and basis sets `s`, and `l'` has a basis indexed by `ι'` with index property `p'` and basis sets `s'`, then `l` and `l'` are disjoint if and only if there exists an index `i` such that `p i` holds and an index `i'` such that `p' i'` holds and the sets `s i` and `s' i'` are disjoint.
In other words, two filters are disjoint if and only if there exists a pair of basis sets, one from each filter, that are disjoint.
More concisely: Two filters on a type, each with a disjoint basis indexed by their respective indices satisfying corresponding index properties, are disjoint if and only if there exist basis sets from each filter that are disjoint.
|
Filter.isCountablyGenerated_principal
theorem Filter.isCountablyGenerated_principal :
∀ {α : Type u_1} (s : Set α), (Filter.principal s).IsCountablyGenerated
This theorem states that for any given set `s` of some type `α`, the principal filter of `s` is countably generated. In other words, the collection of all supersets of `s` (which form the principal filter of `s`) can be generated by a countable collection. In the context of topology, this means that the topology generated by the set `s` is countable. This is significant as countability is a key concept in the study of set theory and topology, and it provides information about the complexity and structure of the set and the topology it generates.
More concisely: The principal filter of any set `s` of type `α` is countably generated. Equivalently, the topology generated by `s` is countable.
|
Filter.hasBasis_biInf_principal
theorem Filter.hasBasis_biInf_principal :
∀ {α : Type u_1} {β : Type u_2} {s : β → Set α} {S : Set β},
DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S →
S.Nonempty → (⨅ i ∈ S, Filter.principal (s i)).HasBasis (fun i => i ∈ S) s
This theorem states that for any types `α` and `β`, a function `s` mapping `β` to sets of `α`, and a set `S` of `β`, if the set `S` is directed with respect to the preimage of the order `(x, x_1) => x ≥ x_1` under function `s`, and if the set `S` is nonempty, then the infimum (or greatest lower bound) of the principal filters of the sets `s i` for `i` in `S` has a filter basis characterized by membership in `S` and mapped by `s`.
In simpler terms, it says that, under certain conditions, we can find a "nice" collection of filters (the basis), determined by the nonempty directed set `S`, that can be used to generate the given infimum of principal filters.
More concisely: Given a nonempty directed set S of beta and a function s from beta to sets of alpha, if the sets si for i in S have a infimum and S is directed under the preorder (x, x'_1) => x >= x'_1, then there exists a filter basis B in S such that the infimum of the principal filters of the sets si for i in B is the same as the infimum of the sets si.
|
Filter.HasBasis.tendsto_left_iff
theorem Filter.HasBasis.tendsto_left_iff :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β}
{f : α → β}, la.HasBasis pa sa → (Filter.Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ Set.MapsTo f (sa i) t)
The theorem `Filter.HasBasis.tendsto_left_iff` states that for all types `α`, `β`, and `ι`, for a given filter `la` on `α`, a filter `lb` on `β`, a function `f` from `α` to `β`, a predicate `pa` on `ι`, and a function `sa` from `ι` to a set of `α`, if `la` has a basis defined by the predicate `pa` and the function `sa`, then the function `f` tends to `lb` along `la` if and only if for every set `t` in the filter `lb`, there exists an index `i` such that `pa i` holds and the image of the set `sa i` under the function `f` is contained in `t`. In other words, it provides a characterization of the notion of the limit of a function with respect to a filter based on the basis of the filter.
More concisely: A function between two types tends to a filter on the codomain along a filter on the domain if and only if the image of the basis elements of the domain filter under the function is contained in each element of the codomain filter.
|
Mathlib.Order.Filter.Bases._auxLemma.22
theorem Mathlib.Order.Filter.Bases._auxLemma.22 : ∀ {α : Type u} (a : α), pure a = Filter.principal {a}
This theorem asserts that for any type `α` and any element `a` of this type, the pure filter of `a` is equivalent to the principal filter of the singleton set containing only `a`. In other words, the collection of all supersets of a singleton set `{a}` is effectively the same as the pure filter of `a`, which, intuitively, is a filter that captures only `a` and nothing else.
More concisely: For any type `α` and element `a` of type `α`, the filter of sets containing `a` (i.e., the principal filter of `{a}`) is equal to the pure filter of `a`.
|
Filter.hasBasis_iff
theorem Filter.hasBasis_iff :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s ↔ ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
This theorem states a property for a filter `l` on a type `α`. It says that a filter `l` has a basis characterized by a predicate `p` and a function `s` from indices of sort `ι` to sets of α, if and only if for every set `t` of elements of type `α`, `t` is in the filter `l` if and only if there exists an index `i` such that `p i` is true and the set `s i` is a subset of `t`. The basis here refers to the fundamental sets that generate the filter. In other words, the filter consists of all sets that include some set `s i` for which the predicate `p i` holds.
More concisely: A filter on type α has a basis consisting of sets `{x ∈ α | p i} for some i and subset s i ⊆ x if and only if for every set t ⊆ α, t ∈ filter iff there exists i such that p i holds and s i ⊆ t.
|
FilterBasis.hasBasis
theorem FilterBasis.hasBasis : ∀ {α : Type u_1} (B : FilterBasis α), B.filter.HasBasis (fun s => s ∈ B) id
This theorem states that for any type `α` and any filter basis `B` on that type, the filter associated with `B` has a basis. The basis is characterized by the property that a set is in the basis if and only if it belongs to `B`. The `id` function is the identity map, which implies that the elements of the basis are directly the sets in `B`. In other words, the filter generated by a filter basis `B` has `B` itself as a basis.
More concisely: For any type `α` and filter basis `B` on `α`, the filter generated by `B` is equal to the filter having `B` as its basis.
|
Filter.HasBasis.eq_of_same_basis
theorem Filter.HasBasis.eq_of_same_basis :
∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → l'.HasBasis p s → l = l'
This theorem states that for any type `α` and index type `ι`, if two filters `l` and `l'` over `α` both have the same basis, where the basis is a family of sets indexed by `ι` and characterized by a certain property `p`, then the two filters `l` and `l'` must be equal. In other words, if two filters have the same basis, they are the same filter.
More concisely: If two filters over a type `α` have the same basis, characterized by property `p`, then they are equal.
|
Filter.basis_sets
theorem Filter.basis_sets : ∀ {α : Type u_1} (l : Filter α), l.HasBasis (fun s => s ∈ l) id
This theorem states that for any filter `l` on a type `α`, the filter has a basis consisting of its own sets. In other words, each set `s` in the filter `l` can be considered a part of the basis for constructing that filter. Here, `Filter.HasBasis l (fun s => s ∈ l) id` means that the filter `l` has a basis where each set is an element of the filter, and the index set is just the identity function.
More concisely: Every filter on a type has itself as its basis.
|
Filter.HasBasis.inf'
theorem Filter.HasBasis.inf' :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
{s' : ι' → Set α},
l.HasBasis p s →
l'.HasBasis p' s' → (l ⊓ l').HasBasis (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd
The theorem `Filter.HasBasis.inf'` states that for any types `α`, `ι`, and `ι'`, and any two filters `l` and `l'` over `α`, indexed by `ι` and `ι'` respectively, along with index-based properties `p` and `p'` and index-based sets `s` and `s'` respectively, if `l` has a basis characterized by predicate `p` and sets `s`, and `l'` has a basis characterized by predicate `p'` and sets `s'`, then the infimum (greatest lower bound) of `l` and `l'` also has a basis. This basis is characterized by the predicate that corresponds to the conjunction of `p` and `p'`, and the set that corresponds to the intersection of `s` and `s'`.
More concisely: If filters `l` and `l'` over type `α`, indexed by `ι` and `ι'` respectively, have bases characterized by predicates `p` and `p'` and sets `s` and `s'` respectively, then their infimum has a basis characterized by the conjunction of `p` and `p'` and the intersection of `s` and `s'`.
|
Filter.HasBasis.property_index
theorem Filter.HasBasis.property_index :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : l.HasBasis p s)
(ht : t ∈ l), p ↑(h.index t ht)
This theorem states that for any filter `l` on a type `α`, index type `ι`, and two functions `p : ι → Prop` and `s : ι → Set α`, if `l` has a basis according to `p` and `s`, and a set `t` belongs to `l`, then the property `p` holds for the index associated with `t`. In other words, if we find the index of a basis set such that `s i ⊆ t` using the `Filter.HasBasis.index` function, the property `p` will hold for this index. This shows a relationship between the filter, its basis, and the properties of the basis elements.
More concisely: For any filter `l` on type `α` with basis according to `p : ι → Prop` and `s : ι → Set α`, if `t ∈ l`, then `p (Filter.HasBasis.index l p s t)` holds.
|
Filter.IsBasis.nonempty
theorem Filter.IsBasis.nonempty :
∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α}, Filter.IsBasis p s → ∃ i, p i
This theorem states that for any type `α` and any type `ι`, and any predicate `p` over `ι` and any function `s` from `ι` to a set of elements of type `α`, if `Filter.IsBasis p s` holds, then there exists at least one `i` in `ι` such that the predicate `p` holds true for `i`. In simpler terms, if `p` and `s` form a filter basis, then there exists an element in the index set `ι` for which the predicate `p` is true.
More concisely: If `(s : ι → α)` is a filter basis for the predicate `p` over `ι`, then there exists an `i ∈ ι` such that `p i` holds.
|
Filter.HasBasis.exists_antitone_subbasis
theorem Filter.HasBasis.exists_antitone_subbasis :
∀ {α : Type u_1} {ι' : Sort u_5} {f : Filter α} [h : f.IsCountablyGenerated] {p : ι' → Prop} {s : ι' → Set α},
f.HasBasis p s → ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
This theorem asserts that if a filter `f` on a type `α` is countably generated and it has a basis characterized by a predicate `p` over the index set `ι'` where each index maps to a set `s` in `α`, then there exists a sequence `x` indexed by the natural numbers (`i : ℕ`) such that `p (x i)` holds for all `i` and the mapping `i => s (x i)` forms a decreasing (antitone) sequence of sets which constitute a basis for the filter `f`. Here, a filter being countably generated means that its elements can be generated from a countable collection of subsets, and a filter having a basis means there is a collection of sets from which every set in the filter can be generated. The decreasing (antitone) condition implies that if `i ≤ j` then the set at index `j` is a subset of the set at index `i`.
More concisely: Given a countably generated filter `f` on type `α` with a countable basis characterized by predicate `p` over index set `ι`, there exists a decreasing sequence `x` indexed by natural numbers such that `p (x i)` holds and `{x i} i ∈ ℕ` forms a basis for `f`.
|
Filter.HasBasis.isBasis
theorem Filter.HasBasis.isBasis :
∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → Filter.IsBasis p s
The theorem `Filter.HasBasis.isBasis` states that for all types `α` and `ι`, a filter `l` of type `α`, and functions `p : ι → Prop` and `s : ι → Set α`, if the filter `l` has a basis characterized by the properties `p` and sets `s`, then `(p, s)` is a basis. This theorem is a part of the framework for working with filters, which are mathematical structures used in various areas of mathematics such as topology and analysis.
More concisely: If a filter on a type `α` has property functions `p : ι → Prop` and set functions `s : ι → Set α` as its basis, then `(p, s)` is the basis for that filter.
|
Filter.IsCountableBasis.countable
theorem Filter.IsCountableBasis.countable :
∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α}, Filter.IsCountableBasis p s → (setOf p).Countable
This theorem states that if we have a countable basis, denoted as `Filter.IsCountableBasis`, determined by a predicate `p` with index set `ι` and a function `s` from `ι` to sets of elements of another type `α`, then the set of indices `i` that satisfy the predicate `p` is countable. The countability is denoted by `(setOf p).Countable`. In simpler terms, it asserts that if we have a basis indexed by countable sets and each index in the basis satisfies a certain condition (predicate `p`), then the set of those indexes is countable.
More concisely: If `p` is a predicate on a countable index set `ι` with a countable basis `s`, then the set of indices `i` such that `p(i)` holds is countable.
|
FilterBasis.nonempty
theorem FilterBasis.nonempty : ∀ {α : Type u_6} (self : FilterBasis α), self.sets.Nonempty
This theorem states that for any given filter basis in any type `α`, the set of base sets for this filter basis is guaranteed to be nonempty. In the context of mathematics, a filter basis is a collection of subsets of a set which generates a filter, and this theorem ensures that no filter basis can be generated from an empty set of subsets.
More concisely: For any filter basis in type `α`, the basis sets are non-empty.
|
Filter.disjoint_principal_right
theorem Filter.disjoint_principal_right :
∀ {α : Type u_1} {f : Filter α} {s : Set α}, Disjoint f (Filter.principal s) ↔ sᶜ ∈ f
This theorem states that, for any given type `α`, any filter `f` on `α`, and any set `s` of `α`, the filter `f` is disjoint with the principal filter of `s` if and only if the complement of `s` is an element of the filter `f`. In the context of lattice theory, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element. Here, the disjointness of `f` and the principal filter of `s` is characterized by the presence of the complement of `s` in `f`. The principal filter of a set `s` is the collection of all supersets of `s`.
More concisely: For any filter `f` on type `α` and set `s` of `α`, `f` is disjoint with the principal filter of `s` if and only if the complement of `s` is in `f`.
|
Filter.HasBasis.prod_same_index
theorem Filter.HasBasis.prod_same_index :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {sa : ι → Set α} {lb : Filter β} {p : ι → Prop}
{sb : ι → Set β},
la.HasBasis p sa →
lb.HasBasis p sb →
(∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) →
(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
The theorem `Filter.HasBasis.prod_same_index` states that for any two types `α` and `β`, an index set `ι`, filters `la` and `lb` on `α` and `β` respectively, and collections of sets `sa`, `sb` indexed by `ι` and a predicate `p` on `ι`, if `la` and `lb` have a basis indexed by `ι` where for `la` the basis sets are given by `sa` and for `lb` the basis sets are given by `sb` such that the predicate `p` holds for the indices of these basis sets, and for any indices `i` and `j` where `p` holds, there exists an index `k` such that `p` holds for `k` and the `k`-th set in `sa` is a subset of the `i`-th set in `sa` and the `k`-th set in `sb` is a subset of the `j`-th set in `sb`, then the product filter `la ×ˢ lb` also has a basis indexed by `ι` where the basis sets are given by the product of the `i`-th set in `sa` and `sb`.
More concisely: If filters `la` and `lb` on types `α` and `β` respectively, indexed by `ι`, have bases `sa` and `sb` satisfying certain conditions, then their product filter `la ×ˢ lb` also has a basis given by the product of the corresponding basis sets `sa` and `sb`.
|