tendsto_indicator_const_apply_iff_eventually
theorem tendsto_indicator_const_apply_iff_eventually :
∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3}
(L : Filter ι) {As : ι → Set α} [inst_2 : T1Space β] (b : β) [inst_3 : NeZero b] (x : α),
Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (nhds (A.indicator (fun x => b) x)) ↔
∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
This theorem states that for a given type `α`, a set `A` of type `α`, a type `β` with `0` and a topology, an index type `ι`, a filter `L` on `ι`, a function `As` from `ι` to sets of `α`, a `T1` topology on `β`, a non-zero element `b` of `β` and an element `x` of `α`, the indicator function of `As i` at `x`, as `i` varies, tends to the indicator function of `A` at `x` if and only if it is eventually true in the filter `L` that `x` is in `As i` if and only if `x` is in `A`.
Here, an indicator function of a set is a function that takes a value specified (`b` in this case) for points in the set and `0` for points not in the set. The notion of 'tends to' is in the sense of filter `L` and the neighborhood filter at the value of the indicator function of `A` at `x`. An event is said to happen `eventually` in a filter if it happens in some set that belongs to the filter.
This can be seen as a condition for the convergence of a sequence of sets to a particular set in a generalized sense according to the filter `L`.
More concisely: For a set `A` of type `α`, a filter `L` on an index type `ι`, and a function `As` from `ι` to sets of `α`, the indicator functions of `As i` at an element `x` of `α` converge to the indicator function of `A` at `x` according to the filter `L` if and only if it is eventually true in `L` that `x` is in `As i` if and only if `x` is in `A`.
|
tendsto_indicator_const_iff_forall_eventually
theorem tendsto_indicator_const_iff_forall_eventually :
∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3}
(L : Filter ι) {As : ι → Set α} [inst_2 : T1Space β] (b : β) [inst_3 : NeZero b],
Filter.Tendsto (fun i => (As i).indicator fun x => b) L (nhds (A.indicator fun x => b)) ↔
∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
The theorem `tendsto_indicator_const_iff_forall_eventually` states that for a given type `α`, a set `A` of type `α`, another type `β` with a zero element and topological space structure, a filter `L` over some type `ι`, and a function `As` from `ι` to a set of `α`, under the condition that `β` is a T1 space and has a non-zero element `b`, the indicator functions of `As i` converge to the indicator function of `A` with respect to the filter `L` if and only if for every element `x` of type `α`, it is eventually true in the filter `L` that `x` belongs to `As i` if and only if `x` belongs to `A`. Here, "eventually" means that the condition holds for all elements outside a certain set in the filter `L`.
More concisely: For a T1 space with a non-zero element and filter over a type, a set's indicator functions converge to the set's indicator function with respect to the filter if and only if for every element, it belongs to the set eventually in the filter if and only if it always belongs to the set.
|