countable_sInter_mem
theorem countable_sInter_mem :
∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)},
S.Countable → (S.sInter ∈ l ↔ ∀ s ∈ S, s ∈ l)
The theorem `countable_sInter_mem` states that for any type `α`, any filter `l` on `α` that supports countable intersection, and any countable set `S` of sets of type `α`, the intersection of all sets in `S` belongs to the filter `l` if and only if every set `s` in `S` belongs to the filter `l`. In other words, for a given type, a filter, and a countable collection of sets, the intersection of the collection is in the filter precisely when every individual set in the collection is in the filter.
More concisely: For any filter `l` on a type `α` that supports countable intersections and any countable set `S` of subsets of `α`, if every `s` in `S` belongs to `l`, then their intersection belongs to `l`.
|
Filter.countableGenerate_isGreatest
theorem Filter.countableGenerate_isGreatest :
∀ {α : Type u_2} (g : Set (Set α)),
IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (Filter.countableGenerate g)
The theorem `Filter.countableGenerate_isGreatest` states that for any type `α` and for any set `g` of sets of type `α`, the function `Filter.countableGenerate` when applied to `g` results in the greatest `countableInterFilter` that contains `g`. This is formalized as `Filter.countableGenerate g` being a greatest element of the set of all filters `f` such that `f` is a `CountableInterFilter` and `g` is a subset of the sets in `f`. This means that `Filter.countableGenerate g` is at least as large as any other `CountableInterFilter` that contains `g`, in the sense of the partial order on filters.
More concisely: The `Filter.countableGenerate` function returns the greatest countable intersecting filter containing a given set.
|
countable_bInter_mem
theorem countable_bInter_mem :
∀ {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_4} {S : Set ι},
S.Countable →
∀ {s : (i : ι) → i ∈ S → Set α}, ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
The theorem `countable_bInter_mem` states that for any type `α` and any filter `l` of type `α`, given that the filter is countable-inter, and for any set `S` of type `ι`, if `S` is countable, then for any function `s` which maps an element `i` of `S` to a set of type `α` (assuming `i` belongs to `S`), the intersection of all sets `s i hi` for each `i` in `S` belongs to the filter `l` if and only if each individual set `s i hi` belongs to `l`.
In other words, the intersection of all sets produced by the function `s` is in the filter `l` if and only if each of these sets is in the filter `l`. This statement is made under the conditions that the filter `l` is countable-inter and the set `S` is countable.
More concisely: For any countable-inter filter `l` on type `α` and countable set `S`, the intersection of images of `S` under a function mapping each element to a set in `l` is in `l` if and only if each image set is in `l`.
|
EventuallyEq.countable_iUnion
theorem EventuallyEq.countable_iUnion :
∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
{s t : ι → Set α}, (∀ (i : ι), l.EventuallyEq (s i) (t i)) → l.EventuallyEq (⋃ i, s i) (⋃ i, t i)
The theorem `EventuallyEq.countable_iUnion` states that for any type `ι` and any type `α`, given a filter `l` on `α` for which countable intersections are defined, and assuming that `ι` is countable, then for any two functions `s` and `t` from `ι` to the set of `α`, if each set `s i` is eventually equal to `t i` with respect to the filter `l` for all `i` in `ι`, then the countable union of all sets `s i` is eventually equal to the countable union of all sets `t i` with respect to the same filter `l`. This theorem relates the concept of eventual equality of sets with the operation of forming countable unions of sets under certain conditions.
More concisely: If `ι` is countable and `l` is a filter on `α` for which countable intersections are defined, then for any two functions `s` and `t` from `ι` to `α`, if each `s i` is eventually equal to `t i` with respect to `l`, then the countable unions of `s` and `t` are eventually equal with respect to `l`.
|
Mathlib.Order.Filter.CountableInter._auxLemma.2
theorem Mathlib.Order.Filter.CountableInter._auxLemma.2 :
∀ {α : Type u_2} {l : Set (Set α)} {hunion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → S.sUnion ∈ l}
{hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l} {s : Set α}, (s ∈ Filter.ofCountableUnion l hunion hmono) = l sᶜ
The theorem `Mathlib.Order.Filter.CountableInter._auxLemma.2` states that for any type `α`, any set `l` of sets of `α`, any set `s` of `α`, given that for any countable set `S` of sets of `α` where each element of `S` is in `l`, the union of `S` is in `l`, and for any set `t` in `l`, any set `s` that is a subset of `t` is in `l`, the statement that `s` is in the filter generated by countable unions from `l` is equivalent to the statement that the complement of `s` is in `l`.
More concisely: For any type `α` and countable set `S` of subsets of `α` in a filter `l`, if every subset of a set in `S` is in `l` and the complement of any set in `l` is also in `l`, then a set is in the filter if and only if its complement is in the filter.
|
eventually_countable_forall
theorem eventually_countable_forall :
∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι]
{p : α → ι → Prop}, (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
The theorem `eventually_countable_forall` states that for any type `α`, filter `l` on `α`, a countable type `ι`, and a property `p` from `α` to `ι`, the statement "For almost every `x` in the filter `l`, for all `i` in `ι`, the property `p` holds for `x` and `i`" is equivalent to the statement "For all `i` in `ι`, for almost every `x` in the filter `l`, the property `p` holds for `x` and `i`". Here, "almost every" refers to the "eventually" notation, meaning that the property holds outside of a set of `l`'s measure zero. The filter `l` is also assumed to have the property that the intersection of any countable collection of sets in `l` is also in `l`.
More concisely: For any type `α`, filter `l` on `α`, countable type `ι`, and property `p` from `α` to `ι`, the properties "for almost every `x` in `l`, `p(x, i)` holds for all `i` in `ι`" and "for all `i` in `ι`, for almost every `x` in `l`, `p(x, i)` holds" are equivalent, given `l`'s countable intersection property.
|
countable_iInter_mem
theorem countable_iInter_mem :
∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α},
⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l
This theorem, `countable_iInter_mem`, states that for any index set ι of any kind (`Sort u_1`), any type `α`, any filter `l` on `α` that satisfies the `CountableInterFilter` condition, and any function `s` mapping from ι to sets of `α`, the intersection of all sets `s i` (for every `i` in ι) is an element of the filter `l` if and only if every set `s i` is an element of `l`. In other words, in a context where countable intersections are preserved, the membership of the intersection of a countable family of sets in a filter is equivalent to the membership of every set in the family.
More concisely: For any index set ι, type α, CountableInterFilter filter l on α, and function s from ι to sets of α, if for all i in ι, s i is in l, then the intersection of all s i is in l.
|
CountableInterFilter.countable_sInter_mem
theorem CountableInterFilter.countable_sInter_mem :
∀ {α : Type u_2} {l : Filter α} [self : CountableInterFilter l] (S : Set (Set α)),
S.Countable → (∀ s ∈ S, s ∈ l) → S.sInter ∈ l
The theorem `CountableInterFilter.countable_sInter_mem` states that for any type `α`, given a filter `l` on `α` and a set `S` of subsets of `α`, if `S` is countable and every subset in `S` belongs to the filter `l`, then the intersection of all subsets in `S` also belongs to the filter `l`. In simpler terms, for a countable collection of sets `s` within a certain filter `l`, their intersection is also a part of `l`.
More concisely: If `l` is a filter on a type `α` and `S ⊆ α` is a countable set of subsets of `α` such that each `s ∈ S` belongs to `l`, then `∩s ∈ l`.
|
Filter.mem_countableGenerate_iff
theorem Filter.mem_countableGenerate_iff :
∀ {α : Type u_2} {g : Set (Set α)} {s : Set α},
s ∈ Filter.countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ S.sInter ⊆ s
The given theorem states that, for any type `α`, any set `g` of sets of `α`, and any set `s` of `α`, `s` belongs to the filter generated by `g` (using countable intersections) if and only if there exists a subset `S` of `g` that is countable and its intersection is a subset of `s`. This theorem provides a condition to check whether a set is in the filter generated by another set where the generator set is used to create the filter through countable intersections.
More concisely: A set belongs to the filter generated by a countable set of sets through countable intersections if and only if it is a subset of some countable intersection of sets in that collection.
|