Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(Topology/Sequences): split file (#10943)
I want to have access to the definitions much earlier. Also, most of the file doesn't need metric spaces at all.
- Loading branch information
Showing
4 changed files
with
159 additions
and
93 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,104 @@ | ||
| /- | ||
| Copyright (c) 2018 Jan-David Salchow. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Jan-David Salchow, Patrick Massot, Yury Kudryashov | ||
| -/ | ||
| import Mathlib.Topology.Defs.Filter | ||
|
|
||
| /-! | ||
| # Sequences in topological spaces | ||
| In this file we define sequential closure, continuity, compactness etc. | ||
| ## Main definitions | ||
| ### Set operation | ||
| * `seqClosure s`: sequential closure of a set, the set of limits of sequences of points of `s`; | ||
| ### Predicates | ||
| * `IsSeqClosed s`: predicate saying that a set is sequentially closed, i.e., `seqClosure s ⊆ s`; | ||
| * `SeqContinuous f`: predicate saying that a function is sequentially continuous, i.e., | ||
| for any sequence `u : ℕ → X` that converges to a point `x`, the sequence `f ∘ u` converges to | ||
| `f x`; | ||
| * `IsSeqCompact s`: predicate saying that a set is sequentially compact, i.e., every sequence | ||
| taking values in `s` has a converging subsequence. | ||
| ### Type classes | ||
| * `FrechetUrysohnSpace X`: a typeclass saying that a topological space is a *Fréchet-Urysohn | ||
| space*, i.e., the sequential closure of any set is equal to its closure. | ||
| * `SequentialSpace X`: a typeclass saying that a topological space is a *sequential space*, i.e., | ||
| any sequentially closed set in this space is closed. This condition is weaker than being a | ||
| Fréchet-Urysohn space. | ||
| * `SeqCompactSpace X`: a typeclass saying that a topological space is sequentially compact, i.e., | ||
| every sequence in `X` has a converging subsequence. | ||
| ## Tags | ||
| sequentially closed, sequentially compact, sequential space | ||
| -/ | ||
|
|
||
| open Set Filter | ||
| open scoped Topology | ||
|
|
||
| variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] | ||
|
|
||
| /-- The sequential closure of a set `s : Set X` in a topological space `X` is the set of all `a : X` | ||
| which arise as limit of sequences in `s`. Note that the sequential closure of a set is not | ||
| guaranteed to be sequentially closed. -/ | ||
| def seqClosure (s : Set X) : Set X := | ||
| { a | ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a) } | ||
| #align seq_closure seqClosure | ||
|
|
||
| /-- A set `s` is sequentially closed if for any converging sequence `x n` of elements of `s`, the | ||
| limit belongs to `s` as well. Note that the sequential closure of a set is not guaranteed to be | ||
| sequentially closed. -/ | ||
| def IsSeqClosed (s : Set X) : Prop := | ||
| ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ n, x n ∈ s) → Tendsto x atTop (𝓝 p) → p ∈ s | ||
| #align is_seq_closed IsSeqClosed | ||
|
|
||
| /-- A function between topological spaces is sequentially continuous if it commutes with limit of | ||
| convergent sequences. -/ | ||
| def SeqContinuous (f : X → Y) : Prop := | ||
| ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, Tendsto x atTop (𝓝 p) → Tendsto (f ∘ x) atTop (𝓝 (f p)) | ||
| #align seq_continuous SeqContinuous | ||
|
|
||
| /-- A set `s` is sequentially compact if every sequence taking values in `s` has a | ||
| converging subsequence. -/ | ||
| def IsSeqCompact (s : Set X) := | ||
| ∀ ⦃x : ℕ → X⦄, (∀ n, x n ∈ s) → ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) | ||
| #align is_seq_compact IsSeqCompact | ||
|
|
||
| variable (X) | ||
|
|
||
| /-- A space `X` is sequentially compact if every sequence in `X` has a | ||
| converging subsequence. -/ | ||
| @[mk_iff] | ||
| class SeqCompactSpace : Prop where | ||
| seq_compact_univ : IsSeqCompact (univ : Set X) | ||
| #align seq_compact_space SeqCompactSpace | ||
| #align seq_compact_space_iff seqCompactSpace_iff | ||
|
|
||
| export SeqCompactSpace (seq_compact_univ) | ||
|
|
||
| /-- A topological space is called a *Fréchet-Urysohn space*, if the sequential closure of any set | ||
| is equal to its closure. Since one of the inclusions is trivial, we require only the non-trivial one | ||
| in the definition. -/ | ||
| class FrechetUrysohnSpace : Prop where | ||
| closure_subset_seqClosure : ∀ s : Set X, closure s ⊆ seqClosure s | ||
| #align frechet_urysohn_space FrechetUrysohnSpace | ||
|
|
||
| /-- A topological space is said to be a *sequential space* if any sequentially closed set in this | ||
| space is closed. This condition is weaker than being a Fréchet-Urysohn space. -/ | ||
| class SequentialSpace : Prop where | ||
| isClosed_of_seq : ∀ s : Set X, IsSeqClosed s → IsClosed s | ||
| #align sequential_space SequentialSpace | ||
|
|
||
| variable {X} | ||
|
|
||
| /-- In a sequential space, a sequentially closed set is closed. -/ | ||
| protected theorem IsSeqClosed.isClosed [SequentialSpace X] {s : Set X} (hs : IsSeqClosed s) : | ||
| IsClosed s := | ||
| SequentialSpace.isClosed_of_seq s hs | ||
| #align is_seq_closed.is_closed IsSeqClosed.isClosed |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,46 @@ | ||
| /- | ||
| Copyright (c) 2018 Jan-David Salchow. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Jan-David Salchow, Patrick Massot, Yury Kudryashov | ||
| -/ | ||
| import Mathlib.Topology.Sequences | ||
| import Mathlib.Topology.MetricSpace.Bounded | ||
|
|
||
| /-! | ||
| # Sequencial compacts in metric spaces | ||
| In this file we prove 2 versions of Bolzano-Weistrass theorem for proper metric spaces. | ||
| -/ | ||
|
|
||
| open Filter Bornology Metric | ||
| open scoped Topology | ||
|
|
||
| variable {X : Type*} [PseudoMetricSpace X] | ||
|
|
||
| @[deprecated lebesgue_number_lemma_of_metric] -- 2024-02-24 | ||
| nonrec theorem SeqCompact.lebesgue_number_lemma_of_metric {ι : Sort*} {c : ι → Set X} {s : Set X} | ||
| (hs : IsSeqCompact s) (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : | ||
| ∃ δ > 0, ∀ a ∈ s, ∃ i, ball a δ ⊆ c i := | ||
| lebesgue_number_lemma_of_metric hs.isCompact hc₁ hc₂ | ||
| #align seq_compact.lebesgue_number_lemma_of_metric SeqCompact.lebesgue_number_lemma_of_metric | ||
|
|
||
| variable [ProperSpace X] {s : Set X} | ||
|
|
||
| /-- A version of **Bolzano-Weistrass**: in a proper metric space (eg. $ℝ^n$), | ||
| every bounded sequence has a converging subsequence. This version assumes only | ||
| that the sequence is frequently in some bounded set. -/ | ||
| theorem tendsto_subseq_of_frequently_bounded (hs : IsBounded s) {x : ℕ → X} | ||
| (hx : ∃ᶠ n in atTop, x n ∈ s) : | ||
| ∃ a ∈ closure s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) := | ||
| have hcs : IsSeqCompact (closure s) := hs.isCompact_closure.isSeqCompact | ||
| have hu' : ∃ᶠ n in atTop, x n ∈ closure s := hx.mono fun _n hn => subset_closure hn | ||
| hcs.subseq_of_frequently_in hu' | ||
| #align tendsto_subseq_of_frequently_bounded tendsto_subseq_of_frequently_bounded | ||
|
|
||
| /-- A version of **Bolzano-Weistrass**: in a proper metric space (eg. $ℝ^n$), | ||
| every bounded sequence has a converging subsequence. -/ | ||
| theorem tendsto_subseq_of_bounded (hs : IsBounded s) {x : ℕ → X} (hx : ∀ n, x n ∈ s) : | ||
| ∃ a ∈ closure s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) := | ||
| tendsto_subseq_of_frequently_bounded hs <| frequently_of_forall hx | ||
| #align tendsto_subseq_of_bounded tendsto_subseq_of_bounded | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters