SeqContinuous.continuous
theorem SeqContinuous.continuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : SequentialSpace X] {f : X → Y}, SeqContinuous f → Continuous f
The theorem states that if a function, defined on a topological space that is also sequential, is sequentially continuous, then it is also continuous. Sequential continuity means that the function preserves the limit of every convergent sequence, and continuity in a topological sense means that the preimage of every open set is open. In other words, given a function `f` from a sequential space `X` to a space `Y` (both equipped with a topological structure), if `f` commutes with the limit of convergent sequences in `X`, then `f` is a continuous function.
More concisely: If a function defined on a sequential topological space is sequentially continuous, then it is continuous.
|
isSeqClosed_iff_isClosed
theorem isSeqClosed_iff_isClosed :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : SequentialSpace X] {M : Set X}, IsSeqClosed M ↔ IsClosed M
The theorem `isSeqClosed_iff_isClosed` states that, in a sequential space (a topological space where sequential convergence implies topological convergence), a set `M` is closed if and only if it's sequentially closed. In other words, a set is closed when it contains all of its limit points, and it's sequentially closed if for any sequence of elements in the set that converges to a limit, the limit also belongs to the set. Therefore, the theorem establishes an equivalence between these two concepts in the context of a sequential space.
More concisely: In a sequential space, a set is closed if and only if it is sequentially closed, i.e., every convergent sequence in the set has its limit as an element of the set.
|
IsSeqCompact.isComplete
theorem IsSeqCompact.isComplete :
∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X} [inst_1 : (uniformity X).IsCountablyGenerated],
IsSeqCompact s → IsComplete s
This theorem states that for any sequentially compact set in a uniform space, if the uniformity filter of the space is countably generated, then the set is also complete. In other words, if every sequence in the set has a converging subsequence and if the uniformity filter is countably generated (i.e., it can be generated by a countable collection of sets), then any Cauchy filter (a filter where every set in the filter contains a "sufficiently close" pair of points) that is a superset of the set will have a limit within the set.
More concisely: If a sequentially compact set in a uniform space is contained in a Cauchy filter generated by a countable collection of sets, then the set is complete.
|
FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto
theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto :
∀ {X : Type u_1} [inst : TopologicalSpace X],
(∀ (f : X → Prop) (a : X),
(∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (nhds a) → Filter.Tendsto (f ∘ u) Filter.atTop (nhds (f a))) →
ContinuousAt f a) →
FrechetUrysohnSpace X
This theorem states a property of Fréchet-Urysohn spaces in topological terms. Specifically, it states that for any topological space `X`, if for every function `f` from `X` to `Prop` and every element `a` of `X`, the condition that whenever a sequence `u` (a mapping from natural numbers to `X`) converges to `a` (i.e., as `u` approaches infinity, it gets arbitrarily close to `a`), it implies that the composition of `f` and `u` also converges to `f(a)`, then the function `f` is continuous at `a`. If this property holds for all such functions and elements, then `X` is a Fréchet-Urysohn space. In mathematical terms, a Fréchet-Urysohn space is a topological space where the limit of a sequence is a point if and only if this point is a limit of a subsequence.
More concisely: In a Fréchet-Urysohn space, if for every function from the space to a proposition and every point, the convergence of sequences implies the convergence of their compositions with the function at that point, then the function is continuous at that point.
|
seqClosure_subset_closure
theorem seqClosure_subset_closure :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, seqClosure s ⊆ closure s
This theorem states that for any set `s` in a topological space `X`, the sequential closure of `s` is a subset of the closure of `s`. The sequential closure of a set `s` is the set of all elements `a` in `X` that can be approached by a sequence of elements in `s`, while the closure of `s` is the smallest closed set that contains `s`. It's important to note that the converse is not true; the closure of a set is not necessarily contained in the sequential closure of the same set.
More concisely: The sequential closure of a set is a subset of its topological closure.
|
IsSeqCompact.isCompact
theorem IsSeqCompact.isCompact :
∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X} [inst_1 : (uniformity X).IsCountablyGenerated],
IsSeqCompact s → IsCompact s
The theorem states that if the uniformity on a type `X` endowed with a `UniformSpace` structure is countably generated (that is, can be generated by a countable collection of sets), then any sequentially compact set in `X` is also compact. In mathematical terms, a set is sequentially compact if every sequence within the set has a converging subsequence and it's compact if for every non-trivial filter that contains the set, there exists a point in the set such that every set of the filter intersects with every neighborhood of that point.
More concisely: If a uniform space X with a countably generated uniformity has every sequentially compact set compact, then X is a completely metrizable and separable topological space. (Note that the given description only states the implication from countably generated uniformity to sequentially compact sets being compact, but the full theorem requires completeness and separability as well.)
|
IsSeqClosed.preimage
theorem IsSeqClosed.preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
IsSeqClosed s → SeqContinuous f → IsSeqClosed (f ⁻¹' s)
This theorem states that the preimage of a sequentially closed set under a sequentially continuous map is also sequentially closed. In mathematical terms, if we have a sequentially closed set `s` in a topological space `Y`, and a sequentially continuous function `f` mapping from another topological space `X` to `Y`, then the preimage of the set `s` under the function `f` (denoted as `f⁻¹(s)`) is sequentially closed in `X`. This means that for any sequence in `f⁻¹(s)` that converges in `X`, its limit also belongs to `f⁻¹(s)`.
More concisely: If `s` is a sequentially closed set in a topological space `Y` and `f` is a sequentially continuous function from a topological space `X` to `Y`, then the preimage `f⁻¹(s)` is a sequentially closed set in `X`.
|
IsSeqClosed.seqClosure_eq
theorem IsSeqClosed.seqClosure_eq :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSeqClosed s → seqClosure s = s
This theorem states that for any type `X` equipped with a topology (`TopologicalSpace X`), and any set `s` of elements from `X`, if `s` is sequentially closed (i.e., every converging sequence of elements in `s` has its limit also in `s`), then the sequential closure of `s` is equal to `s` itself. Here, the sequential closure of a set `s` is defined as the set of all points which can be reached as limits of sequences of elements in `s`. Therefore, if a set is sequentially closed, no new elements are added during the process of taking its sequential closure.
More concisely: A sequentially closed subset of a topological space is equal to its sequential closure.
|
mem_closure_iff_seq_limit
theorem mem_closure_iff_seq_limit :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : FrechetUrysohnSpace X] {s : Set X} {a : X},
a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Filter.Tendsto x Filter.atTop (nhds a)
This theorem states that in a Fréchet-Urysohn space (a type of topological space), a point is in the closure of a set if and only if it is the limit of a sequence where all elements of the sequence are in the set. Specifically, given a type `X` that forms a topological space and is a Fréchet-Urysohn space, a set `s` of elements of type `X`, and a point `a` of type `X`, the theorem asserts that `a` belongs to the closure of `s` if and only if there exists a sequence `x` such that for every natural number `n`, `x n` is an element of `s` and the sequence `x` tends to `a` as `n` goes to infinity.
More concisely: In a Fréchet-Urysohn space, a point is in the closure of a set if and only if it is the limit of a sequence in the set.
|
IsSeqCompact.totallyBounded
theorem IsSeqCompact.totallyBounded :
∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X}, IsSeqCompact s → TotallyBounded s
This theorem states that if a set in a uniform space is sequentially compact, then it is totally bounded. In other words, for any set 's' in a uniform space 'X', if every sequence in 's' has a converging subsequence (i.e., 's' is sequentially compact), then for every entourage 'd' there is a finite set of points such that every element of 's' is 'd'-near to some element of this finite set (i.e., 's' is totally bounded).
More concisely: If a set in a uniform space is sequentially compact, then it is totally bounded. That is, every sequentially compact subset has a finite subcover for every open cover by open balls.
|
IsCompact.isSeqCompact
theorem IsCompact.isSeqCompact :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : FirstCountableTopology X] {s : Set X},
IsCompact s → IsSeqCompact s
This theorem states that for any set `s` in a topological space `X` which also has a first countable topology, if `s` is compact, then `s` is sequentially compact. In other words, if any nontrivial filter containing `s` intersects every neighborhood of some point in `s`, then every sequence of points in `s` has a subsequence that converges to a point in `s`. This theorem is a fundamental result connecting the concepts of compactness and sequential compactness in general topological spaces.
More concisely: In a first countable topological space, every compact set is sequentially compact.
|
seqClosure_eq_closure
theorem seqClosure_eq_closure :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : FrechetUrysohnSpace X] (s : Set X),
seqClosure s = closure s
This theorem states that for any set `s` in a Frechet-Urysohn space `X`, the sequential closure of `s` is equal to the closure of `s`. In other words, in a Frechet-Urysohn space, a point is in the closure of a set if and only if it is the limit of a sequence of points in that set. A Frechet-Urysohn space is a topological space where this property holds true; not all topological spaces have this characteristic.
More concisely: In a Frechet-Urysohn space, the sequential closure of a set equals its closure.
|
isSeqClosed_iff
theorem isSeqClosed_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSeqClosed s ↔ seqClosure s = s
The theorem states that, for any set `s` in a topological space `X`, the set `s` is sequentially closed if and only if it is equal to its sequential closure. In other words, a set `s` is sequentially closed if every sequence in `s` that converges (in the topological sense) has its limit in `s`, and this is equivalent to `s` being equal to the set of all points that can be reached as a limit of sequences in `s`.
More concisely: A set is sequentially closed in a topological space if and only if it equals its sequential closure, i.e., every convergent sequence in the set has its limit in the set.
|
IsClosed.isSeqClosed
theorem IsClosed.isSeqClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → IsSeqClosed s
This theorem states that a set is sequentially closed if it is closed, in any topological space. In other words, for any set `s` within a topological space `X`, if `s` is a closed set, then `s` is also sequentially closed. Sequentially closed means that if we have any sequence of elements in `s` that converges to a limit, the limit itself also belongs to `s`.
More concisely: In any topological space, a closed set is sequentially closed, meaning any convergent sequence in the set has its limit as an element of the set.
|
tendsto_nhds_iff_seq_tendsto
theorem tendsto_nhds_iff_seq_tendsto :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y},
Filter.Tendsto f (nhds a) (nhds b) ↔
∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (nhds a) → Filter.Tendsto (f ∘ u) Filter.atTop (nhds b)
This theorem states that for a given function `f` mapping from a topological space `X` to another topological space `Y`, where `X` is a Fréchet-Urysohn space, the function `f` converges to `b` in the neighborhood of `a` if and only if, for any sequence `u` of elements in `X` that converges to `a`, the sequence formed by mapping `u` through `f` also converges to `b`. Here, convergence is defined in terms of filters: `f` converging to `b` in the neighborhood of `a` means that the image of the neighborhood filter at `a` under `f` is less than or equal to the neighborhood filter at `b`, and a sequence `u` converging to `a` means that the filter of `u` at positive infinity is less than or equal to the neighborhood filter at `a`.
More concisely: For a Fréchet-Urysohn space X and a function f : X -> Y, the function f converges to b in the neighborhood of a if and only if every sequence in X converging to a maps to a converging sequence in Y to b.
|
continuous_iff_seqContinuous
theorem continuous_iff_seqContinuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : SequentialSpace X] {f : X → Y}, Continuous f ↔ SeqContinuous f
This theorem states that for any two topological spaces `X` and `Y`, and for any function `f` from `X` to `Y`, if the topological space `X` is a sequential space (i.e., a space where sequentially convergent sequences determine the topology), then the function `f` is continuous if and only if it is sequentially continuous. In other words, a function is continuous (the pre-images of open sets are open) if and only if it commutes with the limit of convergent sequences. This provides a way of understanding continuity in sequential spaces in terms of the behavior of sequences.
More concisely: A function between two topological spaces is continuous if and only if it preserves the limits of convergent sequences, given that the domain space is a sequential topology.
|
IsSeqCompact.subseq_of_frequently_in
theorem IsSeqCompact.subseq_of_frequently_in :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
IsSeqCompact s →
∀ {x : ℕ → X},
(∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) →
∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
This theorem states that for any given topological space `X` and any set `s` in `X`, if `s` is sequentially compact, then for any sequence `x` of elements in `X` where every element `x(n)` for `n` in natural numbers is frequently in `s` (meaning the set of `n` for which `x(n)` is in `s` is dense in the natural numbers), there exists an element `a` in `s` and a strictly monotone sequence `φ` of natural numbers such that the subsequence of `x` defined by `φ` converges to `a`. In other words, if `s` is sequentially compact and a sequence `x` is frequently in `s`, then `x` has a subsequence which converges to some point in `s`.
More concisely: If a sequentially compact subset `s` of a topological space `X` and a sequence `x` in `X` have density one in `s`, then `x` has a convergent subsequence with limit in `s`.
|
UniformSpace.isCompact_iff_isSeqCompact
theorem UniformSpace.isCompact_iff_isSeqCompact :
∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X} [inst_1 : (uniformity X).IsCountablyGenerated],
IsCompact s ↔ IsSeqCompact s
This theorem, named as `UniformSpace.isCompact_iff_isSeqCompact`, is a version of the Bolzano-Weistrass theorem. It states that in a uniform space with a countably generated uniformity filter (such as in a metric space), a set is compact if and only if it is sequentially compact. In other words, for any type `X` that is a uniform space and any set `s` of type `X`, if the uniformity filter of `X` is countably generated, then `s` is compact if and only if every sequence in `s` has a converging subsequence.
More concisely: In a uniform space with a countably generated uniformity filter, a set is compact if and only if it is sequentially compact.
|
isSeqClosed_of_seqClosure_eq
theorem isSeqClosed_of_seqClosure_eq :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, seqClosure s = s → IsSeqClosed s
This theorem states that if a set is equal to its sequential closure, then it is sequentially closed. In other words, for any topological space `X` and any set `s` of `X`, if every point in `s` can be expressed as the limit of a sequence of points in `s` (that is, if `s` is equal to its sequential closure), then any sequence of points in `s` that converges in `X` has its limit also in `s` (i.e., `s` is sequentially closed).
More concisely: If a set in a topological space is equal to its sequential closure, then it is sequentially closed.
|