UniformCauchySeqOnFilter.comp
theorem UniformCauchySeqOnFilter.comp :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α}
{γ : Type u_1},
UniformCauchySeqOnFilter F p p' →
∀ (g : γ → α), UniformCauchySeqOnFilter (fun n => F n ∘ g) p (Filter.comap g p')
The theorem states that for any given uniform Cauchy sequence on a filter, composing it on the right with a function preserves the property of being a uniform Cauchy sequence. In other words, given a sequence `F` that is uniformly Cauchy on filters `p` and `p'`, and any function `g`, the sequence obtained by composing `F` with `g` is also a uniformly Cauchy sequence on `p` and the filter obtained by mapping `p'` under `g`. Here, a sequence is said to be uniformly Cauchy if, after a certain point, the differences between any two terms in the sequence are uniformly small. This is denoted in Lean by `UniformCauchySeqOnFilter`.
More concisely: For any uniformly Cauchy sequence `F` on filters `p` and `p'`, and any function `g`, the sequence obtained by composing `F` with `g` is also a uniformly Cauchy sequence on the filters `p` and the image filter `g(p')`.
|
tendstoUniformly_iff_tendstoUniformlyOnFilter
theorem tendstoUniformly_iff_tendstoUniformlyOnFilter :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
The theorem `tendstoUniformly_iff_tendstoUniformlyOnFilter` states that, for any sequence of functions `F`, denoted as `F : ι → α → β`, a limiting function `f`, denoted as `f : α → β`, and a filter `p` over `ι`, the sequence `F` converges uniformly to `f` with respect to filter `p` if and only if `F` converges uniformly on the top filter to `f` with respect to the filter `p`. In mathematical terms, this means that for any given entourage of the diagonal `u` in the uniform space `β`, if `p`-eventually `(f x, Fₙ x) ∈ u` for all `x`, then it's also true that `p ×ˢ ⊤`-eventually `(f x, Fₙ x) ∈ u`.
More concisely: For a sequence of functions `F : ι → α → β`, limiting function `f : α → β`, and filter `p` over `ι`, `F` converges uniformly to `f` with respect to `p` if and only if `F` converges uniformly on the top filter to `f` with respect to `p`.
|
TendstoUniformly.prod
theorem TendstoUniformly.prod :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
{ι' : Type u_1} {β' : Type u_2} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'},
TendstoUniformly F f p →
TendstoUniformly F' f' p' →
TendstoUniformly (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p')
The theorem `TendstoUniformly.prod` states that for any two sequences of functions `F` and `F'` that converge uniformly to the limiting functions `f` and `f'` with respect to filters `p` and `p'` respectively, there exists a joint sequence of functions `(F i.1 a, F' i.2 a)` that converges uniformly to the joint limiting function `(f a, f' a)` with respect to the product filter `(p ×ˢ p')`. Here, `α` and `ι` are the domain types, `β` and `β'` are the codomain types equipped with uniform spaces, and `i` is a pair of elements from the filters `p` and `p'`.
More concisely: If sequences `F:` `ι -> β` and `F':` `ι -> β'` uniformly converge to `f:` `α -> β` and `f':` `α -> β'` respectively with respect to filters `p` and `p'`, then there exists a joint sequence `(Fi a, F' i a)` that uniformly converges to the pair `(f a, f' a)` with respect to the product filter `p ×ˢ p'`.
|
UniformCauchySeqOn.prod'
theorem UniformCauchySeqOn.prod' :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
{β' : Type u_1} [inst_1 : UniformSpace β'] {F' : ι → α → β'},
UniformCauchySeqOn F p s → UniformCauchySeqOn F' p s → UniformCauchySeqOn (fun i a => (F i a, F' i a)) p s
This theorem states that for any two sequences `F` and `F'` of type `ι → α → β` and `ι → α → β'` respectively, with `β` and `β'` being types equipped with a uniform space structure, and a filter `p` of type `ι` and a set `s` of type `α`. If `F` and `F'` are both uniformly Cauchy on `p` and `s`, then the sequence formed by pairing the corresponding elements of `F` and `F'` is also uniformly Cauchy on `p` and `s`.
In simpler terms, if we have two sequences that converge uniformly, then the sequence formed by taking pairs of elements from these two sequences also converges uniformly.
More concisely: If `F` and `F'` are two uniformly Cauchy sequences of functions from `ι` to `α` to `β` and `β'` respectively, where `β` and `β'` are uniform spaces, and `p` is a filter on `ι` and `s` is a set of `α`, then the sequence of pairs `(F x) (F' x)` is uniformly Cauchy on `p` and `s`.
|
TendstoLocallyUniformlyOn.continuousOn
theorem TendstoLocallyUniformlyOn.continuousOn :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} [inst_1 : TopologicalSpace α],
TendstoLocallyUniformlyOn F f p s →
(∀ᶠ (n : ι) in p, ContinuousOn (F n) s) → ∀ [inst_2 : p.NeBot], ContinuousOn f s
This theorem states that if we have a sequence of functions `F : ι → α → β` that tends locally uniformly to a function `f : α → β` on a set `s : Set α` with respect to a filter `p : Filter ι`, and if almost every function `F n` in this sequence is continuous on the set `s` for `n` in the filter `p`, then the limit function `f` is continuous on the set `s`, assuming the filter `p` is not bottom. The spaces `α` and `β` are endowed with a topological structure, and `β` is also a uniform space.
More concisely: If a sequence of continuous functions `F : ι → α → β` uniformly converges on a set `s : Set α` to a function `f : α → β` with respect to a non-bottom filter `p : Filter ι`, then `f` is continuous on `s`.
|
UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto
theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
{p' : Filter α} [inst_1 : p.NeBot],
UniformCauchySeqOnFilter F p p' →
(∀ᶠ (x : α) in p', Filter.Tendsto (fun n => F n x) p (nhds (f x))) → TendstoUniformlyOnFilter F f p p'
The theorem states that for any given types `α`, `β`, and `ι`, with `β` being a uniform space, and given a sequence of functions `F` of type `ι → α → β`, a function `f` of type `α → β`, and two filters `p` and `p'` on `ι` and `α` respectively, if `F` is a uniformly Cauchy sequence on the filters `p` and `p'`, and for almost every `x` in `p'`, the sequence `F n x` tends to `f x` according to the neighborhood filter at `f x`, then the sequence of functions `F` converges uniformly to the function `f` with respect to the filters `p` and `p'`. In other words, a uniformly Cauchy sequence of functions converges uniformly to its limit.
More concisely: Given a uniformly Cauchy sequence of functions `F : ι → α → β` with respect to filters `p on ι` and `p' on α`, if for almost every `x` in `p'`, `F n x` converges to `f x` as `n` approaches infinity, then `F` converges uniformly to `f` with respect to `p` and `p'`.
|
TendstoLocallyUniformly.tendsto_comp
theorem TendstoLocallyUniformly.tendsto_comp :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι}
{g : ι → α} [inst_1 : TopologicalSpace α],
TendstoLocallyUniformly F f p →
ContinuousAt f x → Filter.Tendsto g p (nhds x) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
This theorem states that if a sequence of functions `Fₙ` tends locally uniformly to a function `f`, and a sequence `gₙ` tends to a point `x`, then the composition of these sequences, `Fₙ(gₙ)`, tends to `f(x)`. Here, "tends locally uniformly" means that for any small 'entourage' (a form of neighborhood specific to uniform spaces) around a point, we can find a point in the sequence `Fₙ` and a neighborhood of `x`, such that all points `y` in this neighborhood have `(f(y), Fₙ(y))` in our entourage. The "tends to" is with respect to a filter `p`, which essentially captures the notion of limit for the sequences. Furthermore, `f` is assumed to be continuous at `x`, which means that for any neighborhood around `f(x)`, there is a neighborhood around `x` such that the image of this neighborhood under `f` is inside the neighborhood of `f(x)`.
More concisely: If functions `Fₙ : X -> Y`, `gₙ : X -> X`, `f : X -> Y` satisfy `Fₙ` locally uniformly converges to `f`, `gₙ` converges to a point `x`, and `f` is continuous at `x`, then `Fₙ(gₙ)` converges to `f(x)`.
|
TendstoUniformlyOnFilter.uniformCauchySeqOnFilter
theorem TendstoUniformlyOnFilter.uniformCauchySeqOnFilter :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
{p' : Filter α}, TendstoUniformlyOnFilter F f p p' → UniformCauchySeqOnFilter F p p'
The theorem `TendstoUniformlyOnFilter.uniformCauchySeqOnFilter` asserts that for any sequence of functions `F` that converges uniformly on a filter `p'` to a limiting function `f` with respect to the filter `p`, the sequence `F` is also uniformly Cauchy on the filters `p` and `p'`. In other words, if for any entourage of the diagonal `u` one has `p ×ˢ p'`-eventually `(f x, Fₙ x) ∈ u`, then it follows that eventually all pairwise differences of `F` are uniformly bounded, i.e., for any `u` in the uniformity, there exists a point in the filter after which all pairwise differences `(F m, F m')` for `m, m'` in `ι` and `x` in `α`, belong to `u`.
More concisely: If a sequence of functions converges uniformly on filters `p` and `p'` to a limit function, then the sequence is uniformly Cauchy on filter `p`.
|
Mathlib.Topology.UniformSpace.UniformConvergence._auxLemma.6
theorem Mathlib.Topology.UniformSpace.UniformConvergence._auxLemma.6 :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ},
Filter.Tendsto f a (Filter.comap g c) = Filter.Tendsto (g ∘ f) a c
This theorem states that for all types `α`, `β`, and `γ`, and for all functions `f` from `α` to `β`, `g` from `β` to `γ`, and for all filters `a` on `α` and `c` on `γ`, the function `f` tends to the inverse image filter of `g` with respect to `c` as `a` tends to infinity if and only if the composition function `g ∘ f` tends to `c` as `a` tends to infinity. In other words, it states that filtering through `f` and then mapping `g` onto the result is equivalent to composing `g` with `f` and then filtering the result. This codifies a key property of limits in topology and uniform spaces.
More concisely: For all types `α`, `β`, `γ`, functions `f: α → β` and `g: β → γ`, and filters `a on α` and `c on γ`, the filter `f⁁⁃¹(c)` is the limit of `f⁁⁃(a)` if and only if `g ∘ f` tends to `c` as `a` tends to infinity.
|
TendstoUniformlyOnFilter.tendstoUniformlyOn
theorem TendstoUniformlyOnFilter.tendstoUniformlyOn :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι}, TendstoUniformlyOnFilter F f p (Filter.principal s) → TendstoUniformlyOn F f p s
The theorem `TendstoUniformlyOnFilter.tendstoUniformlyOn` states that, given any types `α`, `β`, and `ι` with `β` being a uniform space, any sequence of functions from `ι` to `α → β` denoted by `F`, any function `f` from `α` to `β`, any set `s` of type `α`, and any filter `p` on `ι`, if `F` converges uniformly on the principal filter of `s` towards `f` with respect to the filter `p`, then `F` also converges uniformly on the set `s` towards `f` with respect to the filter `p`. In other words, uniform convergence on the principal filter of a set implies uniform convergence on the set itself.
More concisely: If a sequence of functions converges uniformly on the principal filter of a set to a limit function, then it converges uniformly on the set itself with respect to the same filter.
|
continuousAt_of_locally_uniform_approx_of_continuousAt
theorem continuousAt_of_locally_uniform_approx_of_continuousAt :
∀ {α : Type u} {β : Type v} [inst : UniformSpace β] {f : α → β} {x : α} [inst_1 : TopologicalSpace α],
(∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) → ContinuousAt f x
The theorem `continuousAt_of_locally_uniform_approx_of_continuousAt` states that for any function `f` mapping points from type `α` to type `β` (where `β` is a Uniform Space), if for every "uniform" set `u`, there exists a neighborhood `t` of a point `x` and a function `F` that is continuous at `x`, and for every `y` in `t`, the pair `(f y, F y)` is in `u`, then the function `f` is continuous at the point `x`. In simple terms, if we can approximate a function `f` uniformly by some function `F` that is continuous at `x` around `x`, then `f` is also continuous at `x`.
More concisely: If for every uniform set `u` and for all points `x` in `α`, there exists a neighborhood `t` and a continuous function `F` at `x` such that for all `y` in `t`, `(f y, F y)` is in `u`, then `f` is continuous at `x`.
|
tendstoUniformly_iff_tendsto
theorem tendstoUniformly_iff_tendsto :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
TendstoUniformly F f p ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (uniformity β)
The theorem `tendstoUniformly_iff_tendsto` states that a sequence of functions `Fₙ` converges uniformly to a limiting function `f` with respect to a filter `p` if and only if the function `(n, x) ↦ (f x, Fₙ x)` converges along the product of the filter `p` and the greatest filter (denoted as `⊤`) to the uniformity of `β`. In simpler terms, this theorem provides a condition for uniform convergence of a sequence of functions using the concept of filters and uniformity on a uniform space. It implies that the convergence of the sequence of functions is independent of the behavior of `x` in this limit.
More concisely: A sequence of functions converges uniformly to a limit if and only if the function sending `(n, x)` to the pair of the limit and the sequence value at `x` converges in the product topology.
|
continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt
theorem continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt :
∀ {α : Type u} {β : Type v} [inst : UniformSpace β] {f : α → β} {s : Set α} {x : α} [inst_1 : TopologicalSpace α],
x ∈ s →
(∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) →
ContinuousWithinAt f s x
The theorem `continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt` states that for any types `α` and `β` with `β` being a uniform space, given a function `f` from `α` to `β`, a set `s` of type `α`, and an element `x` of type `α` in the topological space `α` where `x` is an element in the set `s`, if for every filter on the product `β × β` from the uniformity of `β`, there exists a filter on `α` within the neighborhood of `x` in `s` and a function `F` that is continuous at `x` within `s` such that for every `y` in the filter, the pair `(f y, F y)` is in the uniformity filter, then the function `f` is continuous at `x` within the set `s`. In simple terms, if a function can be locally uniformly approximated by functions that are continuous within a set at a point, then the original function is also continuous within that set at that point.
More concisely: If for every filter on the product of a uniform space and itself around a point in a set, there exists a filter on the set and a continuous function on the set that uniformly approximates the original function on the filters, then the original function is continuous at that point within the set.
|
tendstoLocallyUniformlyOn_iff_filter
theorem tendstoLocallyUniformlyOn_iff_filter :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} [inst_1 : TopologicalSpace α],
TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (nhdsWithin x s)
This theorem describes a property of the convergence of a sequence of functions. Specifically, it states that for any types `α`, `β`, and `ι`, and assuming `β` is a uniform space and `α` is a topological space, a sequence of functions `F` from `ι` to `α` to `β` tends to a function `f` from `α` to `β` locally uniformly on a set `s` with respect to a filter `p` if and only if for all `x` in `s`, `F` tends to `f` uniformly on the filter that is the intersection of the neighborhood of `x` and `s` with respect to `p`. In other words, the sequence `F` converges to `f` uniformly on each small neighborhood within `s`.
More concisely: For any types `α`, `β`, and `ι`, if `β` is a uniform space and `α` is a topological space, a sequence of functions `F : ι → α → β` converges locally uniformly to a function `f : α → β` on a set `s` with respect to a filter `p` if and only if for all `x` in `s`, `F` converges uniformly to `f` on the filter of neighborhoods of `x` intersected with `s` with respect to `p`.
|
TendstoUniformlyOn.tendsto_at
theorem TendstoUniformlyOn.tendsto_at :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι}, TendstoUniformlyOn F f p s → ∀ {x : α}, x ∈ s → Filter.Tendsto (fun n => F n x) p (nhds (f x))
This theorem states that if a sequence of functions `Fₙ` converges uniformly to a function `f` on a set `s` with respect to a filter `p`, then, for each point `x` in the set `s`, the function value sequence `Fₙ(x)` converges to `f(x)` in the neighborhood filter of `f(x)`. In other words, uniform convergence of a sequence of functions implies pointwise convergence.
More concisely: If a sequence of functions `Fₙ : X → ℝ` uniformly converges to a function `f : X → ℝ` on a set `X` with respect to a filter `p`, then for all `x` in `X`, `Fₙ(x)` converges to `f(x)` in the neighborhood filter of `f(x)`.
|
TendstoUniformlyOn.tendstoUniformlyOnFilter
theorem TendstoUniformlyOn.tendstoUniformlyOnFilter :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι}, TendstoUniformlyOn F f p s → TendstoUniformlyOnFilter F f p (Filter.principal s)
This theorem states that if a sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` with respect to a filter `p`, then the sequence also converges uniformly on the principal filter of `s` to the same function `f` with respect to the same filter `p`. The principal filter of `s` is a collection of all sets that include `s`. Uniform convergence on a set or a filter means that for any given measure of closeness, all the functions in the sequence are that close to the limiting function in the set or filter after some point in the sequence.
More concisely: If a sequence of functions `Fₙ` uniformly converges to `f` with respect to filter `p` on set `s`, then it also uniformly converges to `f` with respect to the principal filter of `s` using the same filter `p`.
|
UniformContinuous.comp_tendstoUniformly
theorem UniformContinuous.comp_tendstoUniformly :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
{p : Filter ι} [inst_1 : UniformSpace γ] {g : β → γ},
UniformContinuous g → TendstoUniformly F f p → TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p
The theorem `UniformContinuous.comp_tendstoUniformly` states that if we have a function `g` from `β` to `γ` that is uniformly continuous, and a sequence of functions `F` indexed by `ι` that converges uniformly to a function `f` with respect to a filter `p`, then composing `g` with each function in the sequence `F` (and with `f`) also results in a sequence of functions that converges uniformly to the composed function `(g ∘ f)` with respect to the same filter `p`. In other words, left composition with a uniformly continuous function preserves the property of uniform convergence.
More concisely: If `g` is uniformly continuous and `F:` `ι` → `β` → `γ` converges uniformly to `f` with respect to filter `p`, then `g ∘ F:` `ι` → `β` → `γ` converges uniformly to `g ∘ f` with respect to `p`.
|
continuousOn_of_locally_uniform_approx_of_continuousWithinAt
theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt :
∀ {α : Type u} {β : Type v} [inst : UniformSpace β] {f : α → β} {s : Set α} [inst_1 : TopologicalSpace α],
(∀ x ∈ s, ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) →
ContinuousOn f s
This theorem states that if you have a function `f` from one space `α` to a uniform space `β`, and you have a subset `s` of the space `α`, then if for every point `x` in `s` and every neighborhood `u` in the uniformity of `β`, you can find a neighborhood `t` within `s` around `x` and a function `F` which is continuous at `x` within `s` such that every point `y` in `t` is mapped close to its image under `F` (in the sense that `(f y, F y)` belongs to the neighborhood `u`), then `f` is continuous on the subset `s`. In other words, a function is continuous on a set if it can be locally uniformly approximated by functions that are continuous on that set.
More concisely: If a function from a space to a uniform space is locally uniformly approximated by continuous functions on a subset, then the original function is continuous on that subset.
|
TendstoLocallyUniformlyOn.tendsto_comp
theorem TendstoLocallyUniformlyOn.tendsto_comp :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α}
{p : Filter ι} {g : ι → α} [inst_1 : TopologicalSpace α],
TendstoLocallyUniformlyOn F f p s →
ContinuousWithinAt f s x →
x ∈ s → Filter.Tendsto g p (nhdsWithin x s) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
This theorem states that if a sequence of functions `Fₙ` converges locally uniformly to a function `f` on a set `s`, and a sequence `gₙ` converges to a point `x` within `s`, then the sequence `Fₙ(gₙ)` converges to `f(x)` provided that `f` is continuous at `x` within `s` and `x` is an element of `s`. Here, the convergence of `Fₙ` and `gₙ` are with respect to a filter `p`, and the convergence of `Fₙ(gₙ)` is with respect to the neighborhood of `f(x)`.
More concisely: If sequences `{Fn : X → Y}` of functions and `{gn : X → X}` of points converge locally uniformly to `f : X → Y` and `x` on a set `s` with `f` continuous at `x` in `s`, then `Fn(gn)` converges to `f(x)`.
|
TendstoUniformlyOnFilter.prod
theorem TendstoUniformlyOnFilter.prod :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
{p' : Filter α} {ι' : Type u_1} {β' : Type u_2} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'}
{q : Filter ι'},
TendstoUniformlyOnFilter F f p p' →
TendstoUniformlyOnFilter F' f' q p' →
TendstoUniformlyOnFilter (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ q) p'
The theorem `TendstoUniformlyOnFilter.prod` states that given two sequences of functions `F` and `F'` that converge uniformly on a filter `p'` to limiting functions `f` and `f'` respectively, with respect to filters `p` and `q`, then the function that maps each element of the pair `(i, a)` to `(F i.1 a, F' i.2 a)` converges uniformly on the filter `p'` to the limiting function that maps `a` to `(f a, f' a)`, with respect to the product filter `p ×ˢ q`. This is under the condition that the codomain of the functions `F`, `f`, `F'`, and `f'` are uniform spaces.
More concisely: Given uniformly convergent sequences of functions `F : X → Y` and `F' : X' → Y'` on filters `p` and `p'` respectively, with codomain uniform spaces `Y` and `Y'`, their product sequence `(F i.1, F' i.2) : X × X' → Y × Y'` converges uniformly on `p'` to `(f : X → Y, f' : X' → Y')` with `f` and `f'` being the respective limits of `F` and `F'` on filters `p` and `q`.
|
Filter.Tendsto.tendstoUniformlyOnFilter_const
theorem Filter.Tendsto.tendstoUniformlyOnFilter_const :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {p : Filter ι} {g : ι → β} {b : β},
Filter.Tendsto g p (nhds b) → ∀ (p' : Filter α), TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'
The theorem `Filter.Tendsto.tendstoUniformlyOnFilter_const` states that if a sequence `g` converges towards a specific value `b`, then the sequence of constant functions `fun n ↦ fun a ↦ g n` uniformly converges towards the constant function `fun a ↦ b` on any set `s`. In other words, for any set, if each element of a sequence gets arbitrarily close to a specific value, then the sequence of constant functions that maps each element of the sequence to its corresponding element in `g`, also gets arbitrarily close to a constant function that maps each element of the set to `b`. This is true for any filter `p` on the index set and any filter `p'` on the set `s`.
More concisely: If a sequence converges uniformly on a filter to a limit, then the constant sequence formed by mapping each filter element to the sequence limit is the uniform limit of the sequence of constant functions on that filter.
|
TendstoLocallyUniformly.continuous
theorem TendstoLocallyUniformly.continuous :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
[inst_1 : TopologicalSpace α],
TendstoLocallyUniformly F f p → (∀ᶠ (n : ι) in p, Continuous (F n)) → ∀ [inst_2 : p.NeBot], Continuous f
This theorem states that if a sequence of continuous functions, indexed by type `ι`, converges locally uniformly to a limit function `f` with respect to a filter `p`, then the limiting function `f` is also continuous. Here, local uniform convergence is defined with respect to a topology on the domain (type `α`) and a uniform space on the codomain (type `β`). The filter `p` must not be the bottom filter, meaning it must not be the filter which contains all sets.
More concisely: If a sequence of continuous functions indexed by type `ι` converges locally uniformly to a limit function `f` with respect to filter `p` on domain type `α` and uniform space on codomain type `β`, then `f` is also continuous.
|
tendstoUniformlyOn_univ
theorem tendstoUniformlyOn_univ :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
TendstoUniformlyOn F f p Set.univ ↔ TendstoUniformly F f p
This theorem, `tendstoUniformlyOn_univ`, states that for any types `α`, `β`, `ι`, with `β` being a uniform space, and given any sequence of functions `F` from `ι → α → β`, a limiting function `f` from `α → β`, and a filter `p` on `ι`, the sequence `F` converges uniformly on the universal set (i.e., the set of all elements) of `α` to the limiting function `f` with respect to the filter `p` if and only if `F` converges uniformly to `f` with respect to the filter `p`. In other words, the sequence `F` converging uniformly on the universal set is equivalent to `F` converging uniformly in general.
More concisely: For any uniform space β, sequence of functions F : ι → α → β, limiting function f : α → β, and filter p on ι, the sequence F converges uniformly on the universal set of α to f with respect to p if and only if it converges uniformly to f with respect to p.
|
tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact
theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} [inst_1 : TopologicalSpace α],
IsCompact s → (TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s)
This theorem states that for a given compact set 's' in a topological space, the concept of locally uniform convergence on 's' is equivalent to that of uniform convergence on 's'. More explicitly, if we have a sequence of functions 'F' that maps elements from type 'ι' to a function of type 'α' to 'β', as well as a limiting function 'f' (from 'α' to 'β') and a filter 'p' of type 'ι', then 'F' converges to 'f' locally uniformly on the compact set 's' (with respect to filter 'p') if and only if 'F' converges to 'f' uniformly on 's' (with respect to filter 'p'). This is stated under the condition that the set 's' is compact in the topological space.
More concisely: For a compact set 's' in a topological space, a sequence of functions converges locally uniformly to a limit on 's' if and only if it converges uniformly to the limit on 's'.
|
TendstoUniformlyOn.uniformCauchySeqOn
theorem TendstoUniformlyOn.uniformCauchySeqOn :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι}, TendstoUniformlyOn F f p s → UniformCauchySeqOn F p s
The theorem `TendstoUniformlyOn.uniformCauchySeqOn` states that for any given set `s` of some type `α`, for any sequence of functions `F` from `ι` to `α → β`, for a limiting function `f` from `α` to `β`, and for any filter `p` over `ι`, if the sequence `F` converges uniformly to `f` on set `s` with respect to the filter `p`, then this sequence `F` is also a uniformly Cauchy sequence on `s` with respect to the same filter `p`. Here, the term "uniformly" means that the convergence or Cauchy property holds for all elements of the set `s`, and the term "eventually" means that the property holds for all elements past a certain point in the sequence `F`. The type `β` is assumed to have a uniform space structure, which provides the notion of uniform continuity and uniform convergence used in the definitions of uniform convergence and uniform Cauchy property.
More concisely: If a sequence of functions converges uniformly to a limit on a set with respect to a filter, then it is uniformly Cauchy on that set with respect to the same filter.
|
UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto
theorem UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} [inst_1 : p.NeBot],
UniformCauchySeqOn F p s →
(∀ x ∈ s, Filter.Tendsto (fun n => F n x) p (nhds (f x))) → TendstoUniformlyOn F f p s
The theorem states that if we have a sequence of functions `F` that is uniformly Cauchy on a set `s` with respect to a certain filter `p`, and for every element `x` in the set `s`, the sequence `F(n, x)` tends to the limit `f(x)` with respect to the same filter `p`, then the sequence of functions `F` converges uniformly to the function `f` on the set `s` with respect to the filter `p`. In other words, for any entourage of the diagonal `u`, we have `p`-eventually `(f(x), F(n, x)) ∈ u` for all `x ∈ s`. This theorem provides a connection between uniform Cauchy sequences and uniform convergence in the context of topological spaces equipped with a uniform structure (UniformSpace).
More concisely: If a sequence of functions `F` is uniformly Cauchy on a set `s` with respect to filter `p` and for each `x` in `s`, `F(n, x)` converges to `f(x)` with respect to `p`, then `F` uniformly converges to `f` on `s` with respect to `p`.
|
continuousOn_of_uniform_approx_of_continuousOn
theorem continuousOn_of_uniform_approx_of_continuousOn :
∀ {α : Type u} {β : Type v} [inst : UniformSpace β] {f : α → β} {s : Set α} [inst_1 : TopologicalSpace α],
(∀ u ∈ uniformity β, ∃ F, ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) → ContinuousOn f s
The theorem `continuousOn_of_uniform_approx_of_continuousOn` states that for any given function `f` from a type `α` to a type `β` (where `β` has a uniform space structure), and a subset `s` of `α` (where `α` has a topological space structure), if for every uniformity on `β`, there exists a function `F` that is continuous on `s` and such that the pair `(f y, F y)` is in the uniformity for every `y` in `s`, then the function `f` is continuous on `s`. This is equivalent to saying that a function is continuous on a set if it can be uniformly approximated by other functions that are continuous on that set.
More concisely: If for every uniformity on the codomain, there exists a continuous function approximating a given function on a subset, then the given function is continuous on that subset.
|
UniformContinuous.comp_tendstoUniformlyOnFilter
theorem UniformContinuous.comp_tendstoUniformlyOnFilter :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
{p : Filter ι} {p' : Filter α} [inst_1 : UniformSpace γ] {g : β → γ},
UniformContinuous g →
TendstoUniformlyOnFilter F f p p' → TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p'
This theorem states that if you have a uniformly continuous function `g` from type `β` to type `γ`, and a sequence of functions `F` that converges uniformly on a filter `p'` to a limiting function `f` with respect to filter `p`, then composing `g` on the left with `F` and `f` preserves this uniform convergence. In more mathematical terms, if `g` is uniformly continuous and `(Fₙ)` converges uniformly to `f` on a filter `p'` with respect to `p`, then the sequence `(g ∘ Fₙ)` also converges uniformly to `g ∘ f` on `p'` with respect to `p`. The concept of uniform convergence implies that the convergence rate is the same for all points in the space, i.e., it does not depend on the choice of a particular point.
More concisely: If `g` is uniformly continuous from `β` to `γ`, and `F:` (a sequence of functions from `β` to `γ`) converges uniformly to `f` on filter `p'` with respect to filter `p`, then `(g ∘ F)` converges uniformly to `g ∘ f` on `p'` with respect to `p`.
|
continuous_of_locally_uniform_approx_of_continuousAt
theorem continuous_of_locally_uniform_approx_of_continuousAt :
∀ {α : Type u} {β : Type v} [inst : UniformSpace β] {f : α → β} [inst_1 : TopologicalSpace α],
(∀ (x : α), ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) → Continuous f
The theorem `continuous_of_locally_uniform_approx_of_continuousAt` states that if for every point `x` in a topological space `α`, and for every element `u` of the uniformity of a uniform space `β`, there exists a neighborhood `t` of `x` and a function `F` that is continuous at `x` such that for every `y` in `t`, the pair `(f y, F y)` belongs to `u`, then the function `f` from `α` to `β` is continuous. In other words, a function that can be locally uniformly approximated by continuous functions is itself continuous.
More concisely: A function between topological spaces is continuous if it can be locally uniformly approximated by continuous functions.
|
tendstoUniformlyOn_empty
theorem tendstoUniformlyOn_empty :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
TendstoUniformlyOn F f p ∅
The theorem `tendstoUniformlyOn_empty` states that for any given sequence of functions `F` indexed by `ι`, a limiting function `f`, and a filter `p`, the sequence of functions `F` uniformly converges to the function `f` on the empty set, under the given filter `p` in the context of a uniform space `β`. This is declared true vacuously, as there are no points in the empty set to violate the condition for uniform convergence.
More concisely: The empty set universally absorbs uniform convergence of sequences of functions to a limit, in any uniform space.
|
TendstoUniformlyOnFilter.tendsto_at
theorem TendstoUniformlyOnFilter.tendsto_at :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι}
{p' : Filter α},
TendstoUniformlyOnFilter F f p p' → Filter.principal {x} ≤ p' → Filter.Tendsto (fun n => F n x) p (nhds (f x))
This theorem, titled "Uniform convergence implies pointwise convergence," states that for any given types `α`, `β`, and `ι` with `β` being a uniform space, along with functions `F : ι → α → β` and `f : α → β`, an element `x : α`, and filters `p : Filter ι` and `p' : Filter α`. If the sequence of functions `F` converges uniformly on the filter `p'` to the limiting function `f` with respect to the filter `p`, and the principal filter of the set containing only `x` is less than or equal to `p'`, then the function mapping each element of `ι` to `F n x` (the image of `x` under the `n`th function in the sequence) tends under the filter `p` towards the neighborhood filter at `f(x)`. In other words, if a sequence of functions converges uniformly, then the sequence of its function values at any given point will also converge to the function value of the limit function at that point.
More concisely: If a sequence of functions converges uniformly to a limit function on a filter, then the sequence of function values at any point in the domain converges to the limit value of the function at that point.
|
tendstoUniformlyOn_singleton_iff_tendsto
theorem tendstoUniformlyOn_singleton_iff_tendsto :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι},
TendstoUniformlyOn F f p {x} ↔ Filter.Tendsto (fun n => F n x) p (nhds (f x))
The theorem `tendstoUniformlyOn_singleton_iff_tendsto` states that for any types `α`, `β` and `ι`, and given a Uniform Space instance for `β`, a sequence of functions `F` from `ι` to functions from `α` to `β`, a function `f` from `α` to `β`, a filter `p` over `ι`, and a singleton `x` of type `α`, the condition that the function sequence `F` converges uniformly to `f` on `x` with respect to the filter `p` is equivalent to the assertion that the sequence `F` converges to the function `f(x)` at point `x` in the neighborhood filter of `f(x)`. This theorem links the concept of uniform convergence of a sequence of functions to the regular convergence of a sequence of values at a specific point.
More concisely: For any Uniform Space `β`, a sequence `F` of functions from `α to β`, a function `f : α to β`, a filter `p` over `ι`, and a point `x : α`, the sequence `F` converges uniformly to `f` on `x` with respect to `p` if and only if it converges to `f(x)` in the neighborhood filter of `f(x)`.
|
tendsto_prod_principal_iff
theorem tendsto_prod_principal_iff :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {c : β},
Filter.Tendsto (↿F) (p ×ˢ Filter.principal s) (nhds c) ↔ TendstoUniformlyOn F (fun x => c) p s
The theorem `tendsto_prod_principal_iff` states that for all types `α`, `β`, `ι`, for a given uniform space over `β`, a sequence of functions `F` from `ι` to `α → β`, a set `s` of type `α`, a filter `p` over `ι`, and a constant `c` of type `β`, the function `F` tends towards the neighborhood filter of the constant `c` with respect to the product of the filter `p` and the principal filter of the set `s` if and only if the sequence of functions `F` converges uniformly to the constant function that always returns `c` with respect to the filter `p` on the set `s`. This effectively links the concept of uniform convergence of a function sequence to a constant function on a set with the notion of a function tending towards a limit in the topological sense.
More concisely: A sequence of functions from a set to a uniform space tends towards the neighborhood filter of a constant with respect to the product of a filter and the principal filter of the domain if and only if the sequence uniformly converges to the constant function on the domain.
|
TendstoUniformlyOn.tendsto_comp
theorem TendstoUniformlyOn.tendsto_comp :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α}
{p : Filter ι} {g : ι → α} [inst_1 : TopologicalSpace α],
TendstoUniformlyOn F f p s →
ContinuousWithinAt f s x →
Filter.Tendsto g p (nhdsWithin x s) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
The theorem `TendstoUniformlyOn.tendsto_comp` states that if a sequence of functions `F_n` converges uniformly to a function `f` on a set `s`, and another function sequence `g_n` converges to a point `x` within the set `s`, then the composite function sequence `F_n(g_n)` converges to the value `f(x)`, provided that the function `f` is continuous at the point `x` within the set `s`. The convergence of `F_n(g_n)` to `f(x)` is in the sense that for every neighborhood of `f(x)`, after some point, all the function values `F_n(g_n)` fall within that neighborhood. This theorem provides a key result in the study of uniform convergence and continuity in topology and analysis.
More concisely: If functions `F_n` uniformly converge to `f` on set `s`, and sequence `g_n` converges to `x` in `s`, then `F_n(g_n)` converges to `f(x)` provided `f` is continuous at `x` in `s`.
|
TendstoUniformlyOn.comp
theorem TendstoUniformlyOn.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
{s : Set α} {p : Filter ι},
TendstoUniformlyOn F f p s → ∀ (g : γ → α), TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)
This theorem states that for any types `α`, `β`, `γ`, and `ι`, and any uniform space `β`, if a sequence of functions `F` from `ι` to `α → β` converges uniformly on a set `s` of `α` to a limiting function `f` with respect to a filter `p`, then for any function `g` from `γ` to `α`, the sequence of composed functions `F ∘ g` also converges uniformly on the pre-image set `g⁻¹(s)` to the composed limiting function `f ∘ g` with respect to the same filter `p`. In simpler terms, composing on the right by a function preserves the uniform convergence on a set.
More concisely: If a uniformly convergent sequence of functions from `α → β` to `α`, indexed by `ι`, converges uniformly on a set `s subseteq alpha` to a limit function `f`, then the composed sequence `g �Circ F: γ -> beta` (where `g: γ -> alpha`) converges uniformly on `g⁻¹(s)` to the composed function `g ∘ f`.
|
UniformCauchySeqOn.comp
theorem UniformCauchySeqOn.comp :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
{γ : Type u_1}, UniformCauchySeqOn F p s → ∀ (g : γ → α), UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)
The given theorem, `UniformCauchySeqOn.comp`, states that if we have a uniformly Cauchy sequence `F` on a set `s` under a filter `p` in a uniform space `β`, then for any function `g` from a type `γ` to `α`, the composition of `F` and `g` is also a uniformly Cauchy sequence on the preimage of `s` under `g`, under the same filter `p`. In simpler terms, right-composition with a function preserves the property of being a uniformly Cauchy sequence.
More concisely: If `F` is a uniformly Cauchy sequence of functions from a set `s` to a uniform space `β` under filter `p`, then the composition `g ∘ F` is a uniformly Cauchy sequence of functions from the preimage `g⁁ⁱ⁻¹(s)` to `β` under filter `p`.
|
TendstoUniformlyOn.tendstoLocallyUniformlyOn
theorem TendstoUniformlyOn.tendstoLocallyUniformlyOn :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} [inst_1 : TopologicalSpace α], TendstoUniformlyOn F f p s → TendstoLocallyUniformlyOn F f p s
This theorem states that for any types `α`, `β`, and `ι`, with `β` having a uniform space structure and `α` having a topological space structure, if a sequence of functions `F : ι → α → β` converges uniformly on a set `s` of type `α` to a limiting function `f : α → β` with respect to a filter `p` of type `ι`, then the sequence of functions `F` also converges locally uniformly on the set `s` to the limiting function `f`. In terms of mathematics, given any entourage of the diagonal, we can find an index in the filter such that for all subsequent indices, the function values are in the entourage for all points in the set.
More concisely: Given a uniform space `(β, ε)`, a topological space `(α, τ)`, a convergent uniformly sequence of functions `F : ι → α → β`, and a filter `p` on `ι`, if `F` converges uniformly on `s subseteq α` to `f : α → β` with respect to `p`, then `F` converges locally uniformly on `s` to `f`.
|
tendsto_comp_of_locally_uniform_limit_within
theorem tendsto_comp_of_locally_uniform_limit_within :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α}
{p : Filter ι} {g : ι → α} [inst_1 : TopologicalSpace α],
ContinuousWithinAt f s x →
Filter.Tendsto g p (nhdsWithin x s) →
(∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) →
Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
This theorem states that if a sequence of functions `Fₙ` converges locally uniformly on a neighborhood of a point `x` within a set `s` to a function `f` which is continuous at `x` within `s`, and each `gₙ` in a sequence `g` tends to `x` within `s`, then the value of the sequence of functions `Fₙ` evaluated at `gₙ` tends to the value of `f` at `x`. Here, the convergence of `Fₙ` is measured with respect to the uniformity of the target space `β`, and the sequence `g` is indexed by some type `ι` in a filter `p`.
More concisely: If a sequence of continuous functions `Fₙ : β → X` on a set `X` converges uniformly on a neighborhood of `x` in a set `s` to a continuous function `f : β → X`, and a sequence `gₙ` in `s` converges to `x` in `s`, then `Fₙ(gₙ)` converges to `f(x)`.
|
TendstoUniformlyOn.prod
theorem TendstoUniformlyOn.prod :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} {ι' : Type u_1} {β' : Type u_2} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'}
{p' : Filter ι'},
TendstoUniformlyOn F f p s →
TendstoUniformlyOn F' f' p' s →
TendstoUniformlyOn (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p.prod p') s
The theorem `TendstoUniformlyOn.prod` states that given two sequences of functions, `F` and `F'`, which converge uniformly to limiting functions `f` and `f'` on a set `s` with respect to filters `p` and `p'` respectively, the sequence of functions `(F i.1 a, F' i.2 a)` converges uniformly to the limiting function `(f a, f' a)` on the same set `s` with respect to the product of filters `p` and `p'`. This theorem essentially states that the uniform convergence of a sequence of functions is preserved under the product operation.
More concisely: Given sequences of functions `F` and `F'` that uniformly converge to `f` and `f'` on set `s` with respect to filters `p` and `p'` respectively, `F.product` (`F i.1 _ _, F' i.2 _ _`) uniformly converges to the product function `f * f'` on `s` with respect to the product filter `p ⊓ p'`.
|
TendstoUniformlyOnFilter.comp
theorem TendstoUniformlyOnFilter.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
{p : Filter ι} {p' : Filter α},
TendstoUniformlyOnFilter F f p p' →
∀ (g : γ → α), TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (Filter.comap g p')
The theorem states that for any types `α`, `β`, `γ`, and `ι`, where `β` is a uniform space, sequence of functions `F` from `ι` to `α` to `β`, a limiting function `f` from `α` to `β`, and filters `p` over `ι` and `p'` over `α`, if `F` converges uniformly to `f` with respect to `p` and `p'`, then for any function `g` from `γ` to `α`, `F` composed with `g` also converges uniformly to `f` composed with `g` with respect to `p` and the filter over `γ` that is the preimage of `p'` under `g`. In mathematical terms, if $(F_n)$ converges uniformly to $f$ over a filter, then $(F_n \circ g)$ also converges uniformly to $(f \circ g)$ over the preimage of the filter under $g$.
More concisely: If functions $F:\ íto\ álto\ β$ and $f:\ álto\ β$ converge uniformly to each other with respect to filters $p$ over $ír$ and $p'$ over $ál$, and $g:\ γto\ ál$, then $F\circ g$ converges uniformly to $f\circ g$ with respect to $p$ and the filter on $\gamma$ induced by $p'$.
|
UniformCauchySeqOn.cauchy_map
theorem UniformCauchySeqOn.cauchy_map :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {x : α} {p : Filter ι}
[hp : p.NeBot], UniformCauchySeqOn F p s → x ∈ s → Cauchy (Filter.map (fun i => F i x) p)
The theorem `UniformCauchySeqOn.cauchy_map` states that if we have a sequence of functions, denoted by `F`, that is uniformly Cauchy on a set `s`, then for any point `x` in the set `s`, the sequence of values `F i x` (for each `i` in the indexing set under a filter `p`) forms a Cauchy sequence. This is under the precondition that the filter `p` is not bottom (i.e., `p` is not the filter that contains all sets). The definition of a Cauchy sequence here is generalised to filters: a filter is Cauchy If for every entourage, there exists a set in the filter such that the product of the set with itself is a subset of the entourage.
More concisely: If `F` is a uniformly Cauchy sequence of functions on a set `s` under a non-bottom filter `p`, then for each `x` in `s`, the sequence `F i x` forms a Cauchy sequence with respect to `p`.
|
TendstoUniformly.comp
theorem TendstoUniformly.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
{p : Filter ι}, TendstoUniformly F f p → ∀ (g : γ → α), TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p
The theorem states that if a sequence of functions `F` converges uniformly to a function `f` with respect to a filter `p`, then compositional application of another function `g` on `F` and `f` will also converge uniformly with respect to the same filter `p`. In other words, if for any "closeness" criterion `u`, there is a point in the filter `p` beyond which all `F` are "close" to `f` (i.e., `(f x, F n x) ∈ u` for all `x`), then the same property applies for their composition with `g`. This essentially means that uniform convergence is preserved under function composition.
More concisely: If a sequence of functions `F` uniformly converges to `f` with respect to a filter `p`, then the composition of `g` with each `F` in the sequence and with `f` uniformly converges to `g ∘ f` with respect to `p`.
|
TendstoUniformly.tendsto_comp
theorem TendstoUniformly.tendsto_comp :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι}
{g : ι → α} [inst_1 : TopologicalSpace α],
TendstoUniformly F f p →
ContinuousAt f x → Filter.Tendsto g p (nhds x) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
This theorem states that if you have a sequence of functions `Fₙ`, that tends uniformly to a function `f`, and a sequence `gₙ` that tends to a point `x`, then the composition `Fₙ gₙ` of these sequences also has a limit and it tends to `f x`. More specifically, for every neighborhood of `f x`, the `Fₙ gₙ`-preimage of this neighborhood is eventually in the `p` filter, meaning that for all sufficiently large `n`, the values `Fₙ gₙ` are in this neighborhood of `f x`. This theorem connects the concepts of uniform convergence of a sequence of functions and the limit of a function at a point in a topological space, and shows how they interact in the context of function composition.
More concisely: If `(Fₙ: X → Y)_` is a uniformly convergent sequence of functions to `f: X → Y`, and `(gₙ: X → ℝ)_` is a sequence converging to a point `x ∈ X`, then `(Fₙ ∘ gₙ)` converges to `f x`.
|
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter
theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι}, TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (Filter.principal s)
This theorem states that for any type `α`, `β`, and `ι`, with `β` having a uniform space structure, any sequence of functions `F` from `ι` to `α → β`, a function `f` from `α` to `β`, a set `s` of type `α`, and a filter `p` over `ι`, the condition that `F` converges uniformly to `f` on `s` with respect to `p` is equivalent to the condition that `F` converges uniformly to `f` on the principal filter of `s` with respect to `p`. In other words, uniform convergence of a sequence of functions on a set is the same as uniform convergence on the principal filter of that set.
More concisely: For any type `α`, `β`, and `ι`, with `β` having a uniform space structure, the sequence of functions `F` from `ι` to `α → β` converges uniformly to `f` on a set `s` of type `α` with respect to filter `p` over `ι` if and only if it converges uniformly on the principal filter of `s` with respect to `p`.
|
TendstoUniformlyOn.mono
theorem TendstoUniformlyOn.mono :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} {s' : Set α}, TendstoUniformlyOn F f p s → s' ⊆ s → TendstoUniformlyOn F f p s'
The theorem `TendstoUniformlyOn.mono` states that for any types `α`, `β`, and `ι`, with `β` being a uniform space, given a sequence of functions `F` from `ι` to `α → β`, a limiting function `f` from `α` to `β`, a filter `p` on `ι`, and two sets `s` and `s'` of `α`, if the sequence `F` converges uniformly on set `s` to the function `f` with respect to the filter `p`, and if `s'` is a subset of `s`, then the sequence `F` also converges uniformly on the subset `s'` to the function `f` with respect to the same filter `p`. In other words, the uniform convergence of a sequence of functions on a set implies its uniform convergence on any subset of that set.
More concisely: If a sequence of functions converges uniformly on a set and a subset of that set, then the uniform convergence holds on the subset as well.
|
TendstoUniformlyOn.continuousOn
theorem TendstoUniformlyOn.continuousOn :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
{p : Filter ι} [inst_1 : TopologicalSpace α],
TendstoUniformlyOn F f p s → (∀ᶠ (n : ι) in p, ContinuousOn (F n) s) → ∀ [inst_2 : p.NeBot], ContinuousOn f s
This theorem states that if a sequence of functions `Fₙ`, which are continuous on a set `s`, converges uniformly to a limiting function `f` on the set `s` with respect to a certain filter `p`, then the limiting function `f` is itself continuous on the set `s`. This holds under the condition that the filter `p` is not bottom, which means that it does not map all sets to false. In the context of topological spaces, the theorem demonstrates the preservation of continuity under the process of uniform convergence.
More concisely: If `Fₙ` is a uniformly convergent sequence of continuous functions on a set `s` with respect to a non-bottom filter `p`, then the limiting function `f` is also continuous on `s`.
|
TendstoUniformly.continuous
theorem TendstoUniformly.continuous :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
[inst_1 : TopologicalSpace α],
TendstoUniformly F f p → (∀ᶠ (n : ι) in p, Continuous (F n)) → ∀ [inst_2 : p.NeBot], Continuous f
The theorem `TendstoUniformly.continuous` states that if a sequence of continuous functions `{Fₙ}` converges uniformly to a limit function `f` with respect to a non-bottom filter `p`, then this limit function `f` is also continuous. The uniform convergence is defined such that for any entourage of the diagonal `u`, one has `p`-eventually `(f x, Fₙ x) ∈ u` for all `x`. This theorem highlights an important property of uniform convergence, namely its preservation of continuity.
More concisely: If a sequence of continuous functions converges uniformly to a limit function with respect to a non-bottom filter, then the limit function is also continuous.
|
tendsto_prod_top_iff
theorem tendsto_prod_top_iff :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {c : β},
Filter.Tendsto (↿F) (p ×ˢ ⊤) (nhds c) ↔ TendstoUniformly F (fun x => c) p
The theorem `tendsto_prod_top_iff` states that, for any type `α`, `β`, `ι` and any uniform space on `β`, given a sequence of functions `F` from `ι` to `α` to `β`, a filter `p` on `ι`, and a constant `c` of type `β`, the function `F` tends to the filter `nhds c` (the neighborhood filter of `c`) along the product filter of `p` and the top filter if and only if the sequence of functions `F` converges uniformly to the constant function that always returns `c` with respect to the filter `p`. In terms of analysis, this is saying that uniform convergence of a sequence of functions to a constant function is equivalent to the pointwise convergence of the sequence to the constant in the product space.
More concisely: A sequence of functions from a type to another uniform space converges uniformly to a constant function if and only if the functions tend to the neighborhood filter of the constant in the product of the filter and the top filter.
|
TendstoUniformly.tendsto_at
theorem TendstoUniformly.tendsto_at :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
TendstoUniformly F f p → ∀ (x : α), Filter.Tendsto (fun n => F n x) p (nhds (f x))
The theorem `TendstoUniformly.tendsto_at` states that if a sequence of functions `F` converges uniformly to a limiting function `f` with respect to a particular filter `p`, then for each point `x` in the domain, the sequence of values `F n x` also converges in the standard sense (i.e., pointwise) to `f x` with respect to the same filter. This theorem essentially captures the idea that uniform convergence of a sequence of functions implies pointwise convergence.
More concisely: If a sequence of functions `F: X → ℝ` uniformly converges to a limit function `f: X → ℝ` with respect to a filter `p` on `X`, then `F n x` converges pointwise to `f x` for all `x` in `X` with respect to `p`.
|
continuous_of_uniform_approx_of_continuous
theorem continuous_of_uniform_approx_of_continuous :
∀ {α : Type u} {β : Type v} [inst : UniformSpace β] {f : α → β} [inst_1 : TopologicalSpace α],
(∀ u ∈ uniformity β, ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u) → Continuous f
The theorem `continuous_of_uniform_approx_of_continuous` states that if we have a function `f` from a topological space `α` into a uniform space `β`, and for every set `u` in the uniformity of `β` we can find a continuous function `F` such that every output pair `(f y, F y)` for all `y` in `α` is in `u`, then `f` itself is continuous. In simpler terms, if a function can be approximated uniformly by continuous functions, then the function itself is continuous.
More concisely: If a function from a topological space into a uniform space can be uniformly approximated by continuous functions, then it is continuous.
|
tendstoUniformlyOn_iff_tendsto
theorem tendstoUniformlyOn_iff_tendsto :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
{s : Set α},
TendstoUniformlyOn F f p s ↔
Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ Filter.principal s) (uniformity β)
This theorem states that a sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` with respect to a filter `p` if and only if the function `(n, x) ↦ (f x, Fₙ x)` converges from the product of the filter `p` and the principal filter of `s` to the uniformity. In simpler terms, it's stating a condition under which we can say that a sequence of functions is converging uniformly on a particular set to a limit function. The condition is essentially that a certain map, which takes a pair consisting of an index and an element of the set, and produces a pair of the limit function evaluated at the element, and the indexed function evaluated at the element, is converging to the uniformity of the codomain.
More concisely: A sequence of functions `Fₙ : X → Y` converges uniformly to `f : X → Y` with respect to filter `p` on `X` if and only if the function `(n, x) ↦ (f x, Fₙ x) : p × principalFilter X → Y × Y` converges to the uniformity on the product `p × principalFilter X`.
|
UniformContinuousOn.tendstoUniformly
theorem UniformContinuousOn.tendstoUniformly :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace β] [inst_1 : UniformSpace α] [inst_2 : UniformSpace γ]
{x : α} {U : Set α},
U ∈ nhds x → ∀ {F : α → β → γ}, UniformContinuousOn (↿F) (U ×ˢ Set.univ) → TendstoUniformly F (F x) (nhds x)
This theorem states that for all types `α`, `β`, and `γ` equipped with uniform spaces, given a point `x` of type `α` and a set `U` of type `α` which is a neighborhood of `x`, and a function `F` from `α` to the space of functions from `β` to `γ`, if `F` is uniformly continuous on the product of the set `U` and the universal set of `β`, then the sequence of functions `F` converges uniformly to the function `F(x)` with respect to the neighborhood filter of `x`.
In simpler terms, if `F` is uniformly continuous when `x` is in a neighborhood `U`, then as `x` gets closer and closer to a point in the neighborhood, `F(x)` will get closer and closer to a limit function at a uniform rate, regardless of where `x` is in the neighborhood.
More concisely: If `F` is a uniformly continuous function from the product of a neighborhood `U` of a point `x` in type `α` and the universal set of `β` to the space of functions from `β` to `γ`, then `F` converges uniformly to `F(x)` with respect to the neighborhood filter of `x`.
|
UniformContinuous.comp_uniformCauchySeqOn
theorem UniformContinuous.comp_uniformCauchySeqOn :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {s : Set α}
{p : Filter ι} [inst_1 : UniformSpace γ] {g : β → γ},
UniformContinuous g → UniformCauchySeqOn F p s → UniformCauchySeqOn (fun n => g ∘ F n) p s
This theorem states that if you have a uniformly continuous function `g` from some type `β` to another type `γ`, and a sequence `F` from type `ι` to a function from type `α` to `β` that is uniformly Cauchy on a set `s` with respect to a filter `p`, then the sequence obtained by composing `g` and `F` (i.e., applying `g` to the output of `F`) is also uniformly Cauchy on the set `s` with respect to the same filter `p`. This is essentially saying that uniformly continuous functions preserve the property of being a uniformly Cauchy sequence when applied to elements of such a sequence.
More concisely: If `g` is uniformly continuous from `β` to `γ`, and `F : ι → α → β` is a uniformly Cauchy sequence of functions with respect to filter `p`, then `g ∘ F : ι → γ` is also a uniformly Cauchy sequence with respect to `p`.
|
Filter.Tendsto.tendstoUniformlyOn_const
theorem Filter.Tendsto.tendstoUniformlyOn_const :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {p : Filter ι} {g : ι → β} {b : β},
Filter.Tendsto g p (nhds b) → ∀ (s : Set α), TendstoUniformlyOn (fun n x => g n) (fun x => b) p s
This theorem asserts that if a sequence `g` converges to a value `b`, then the sequence of constant functions constructed from `g` (i.e., each function in the sequence takes any input `a` and returns `g(n)`) uniformly converges to a constant function that always returns `b`, no matter the set `s` on which this is considered. In other words, the behavior of the sequence `g` is extended to a sequence of functions in a way that preserves the original sequence's limit.
More concisely: If a sequence `g` converges to a limit `b` in a set `X`, then the sequence of constant functions `fun x => g n` converges uniformly to the constant function `fun x => b` on `X`.
|
UniformContinuous.comp_tendstoUniformlyOn
theorem UniformContinuous.comp_tendstoUniformlyOn :
∀ {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
{s : Set α} {p : Filter ι} [inst_1 : UniformSpace γ] {g : β → γ},
UniformContinuous g → TendstoUniformlyOn F f p s → TendstoUniformlyOn (fun i => g ∘ F i) (g ∘ f) p s
This theorem states that if we have a uniformly continuous function `g` from `β` to `γ`, and a sequence of functions `F` that converges uniformly on a set `s` to a limiting function `f` with respect to some filter `p`, then composing each function in the sequence `F` with `g` will also converge uniformly on the same set `s` to the function obtained by composing `f` with `g` with respect to the same filter `p`. This basically means that left composition preserves the property of uniform convergence on a set.
More concisely: If `g` is uniformly continuous from `β` to `γ`, `F: Array α -> β` converges uniformly on set `s` to `f` with respect to filter `p`, then the composed functions `g ∘ F` converge uniformly on `s` to `g ∘ f` with respect to `p`.
|
tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace
theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
[inst_1 : TopologicalSpace α] [inst_2 : CompactSpace α], TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
The theorem `tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace` states that for a compact space, the concept of locally uniform convergence is equivalent to uniform convergence. More specifically, given a sequence of functions `Fₙ` from an index set `ι` to a function space `α → β`, a limiting function `f : α → β`, and a filter `p` on `ι`, in a compact topological space `α` and for a uniform space `β`, the sequence `Fₙ` converges locally uniformly to `f` with respect to the filter `p` if and only if `Fₙ` converges uniformly to `f` with respect to the same filter `p`.
More concisely: In a compact topological space with uniform convergence, locally uniform convergence and uniform convergence of a sequence of functions are equivalent.
|
tendsto_comp_of_locally_uniform_limit
theorem tendsto_comp_of_locally_uniform_limit :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι}
{g : ι → α} [inst_1 : TopologicalSpace α],
ContinuousAt f x →
Filter.Tendsto g p (nhds x) →
(∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) →
Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
The theorem `tendsto_comp_of_locally_uniform_limit` states that if a sequence of functions `Fₙ` converges locally uniformly on a neighborhood of a point `x` to a function `f` that is continuous at `x`, and a sequence `gₙ` converges to `x`, then the composed sequence `Fₙ (gₙ)` converges to `f(x)`. Here, local uniform convergence means that for every entourage (a set of all pairs of points that are "close" to each other) in the uniformity of the codomain `β`, there exists a neighborhood of `x` such that for all "later" elements of the sequence indexed by `ι`, the images `Fₙ(y)` and `f(y)` lie within the given entourage for all points `y` in the neighborhood. Hence, as `gₙ` approaches `x`, the value `Fₙ(gₙ)` gets arbitrarily close to `f(x)`, formalizing the concept of the limit of the composed sequence.
More concisely: If sequences of functions `Fₙ : X → β` and `gₙ : X → ℝ` converge with `Fₙ` locally uniformly to a continuous function `f : X → β` at a point `x ∈ X` and `gₙ` to `x`, then `Fₙ ∘ gₙ` converges to `f(x)`.
|
uniformCauchySeqOn_iff_uniformCauchySeqOnFilter
theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι},
UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (Filter.principal s)
The theorem `uniformCauchySeqOn_iff_uniformCauchySeqOnFilter` establishes an equivalence between two forms of uniform Cauchy sequences. Specifically, for any type `α`, type `β` with a uniform space structure, type `ι`, a function `F` mapping from `ι` and `α` to `β`, a set `s` of type `α`, and a filter `p` on `ι`, the function `F` combined with filter `p` forms a uniformly Cauchy sequence on set `s` if and only if it forms a uniformly Cauchy sequence on the principal filter of set `s`. Essentially, this theorem provides a bridge between a set-based and a filter-based definition of uniform Cauchy sequences.
More concisely: For any uniform space `(β, δ)`, type `α`, filter `p` on `ι`, set `s subseteq α`, function `F : ι -> α -> β`, the sequence `{F x | x in s}` is uniformly Cauchy with respect to `p` if and only if it is uniformly Cauchy with respect to the principal filter of `s`.
|
tendstoUniformlyOnFilter_iff_tendsto
theorem tendstoUniformlyOnFilter_iff_tendsto :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
{p' : Filter α},
TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (uniformity β)
This theorem states that a sequence of functions `Fₙ` converges uniformly on a filter `p'` to a limiting function `f` with respect to filter `p` if and only if the function that maps a pair `(n, x)` to `(f x, Fₙ x)` converges along the product filter `p ×ˢ p'` to the uniformity of the space `β`. In other words, the theorem tells us that in this limit, `x` behaves in a way determined solely by the filter `p'`.
More concisely: A sequence of functions `Fₙ` converges uniformly on a filter `p'` to a limiting function `f` with respect to filter `p` if and only if the function that maps `(n, x)` to `(f x, Fₙ x)` converges along the product filter `p ×ˢ p'` to the uniformity of the space.
|
tendsto_prod_filter_iff
theorem tendsto_prod_filter_iff :
∀ {α : Type u} {β : Type v} {ι : Type x} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α}
{c : β}, Filter.Tendsto (↿F) (p ×ˢ p') (nhds c) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'
The theorem `tendsto_prod_filter_iff` states that for any types `α`, `β`, and `ι` (which can be thought of as the domains of sequences of functions, their limit function, and the indexes of the sequence respectively) with `β` equipped with a uniform space structure, a given sequence of functions `F` indexed by `ι` from `α` to `β`, and given filters `p` on `ι` and `p'` on `α`, and a constant `c` in `β`, the function `F` tends to the constant function equal to `c` uniformly on the filter `p'` if and only if the sequence of functions `F`, when considered as a map from the product of `p` and `p'` to `β`, tends towards the constant `c` in the neighborhood filter of `c`. In simpler terms, it relates uniform convergence of a sequence of functions to a constant function with the convergence of the sequence in the product filter.
More concisely: A sequence of functions from `α` to `β` uniformly converges to a constant `c` in `β` if and only if the sequence, viewed as a function from the product of filters on `α` and `β`, tends to `c` in the neighborhood filter of `c`.
|