ultrafilter_isClosed_basic
theorem ultrafilter_isClosed_basic : ∀ {α : Type u} (s : Set α), IsClosed {u | s ∈ u}
The theorem states that for any type `α` and any set `s` of elements of type `α`, the collection of ultrafilters `u` for which `s` is a member of `u` is a closed set in the topological space of ultrafilters. In other words, the basic open sets in the topology on ultrafilters are also closed sets.
More concisely: The collection of ultrafilters containing a given set is a closed set in the topology of ultrafilters.
|
ultrafilter_extend_extends
theorem ultrafilter_extend_extends :
∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [inst_1 : T2Space γ] (f : α → γ),
Ultrafilter.extend f ∘ pure = f
The theorem `ultrafilter_extend_extends` states that for any types `α` and `γ`, where `γ` is a topological space and a T2 space (also known as a Hausdorff space), and given any function `f` from `α` to `γ`, the composition of `Ultrafilter.extend f` and `pure` is equal to `f`. In other words, the extension of the function `f` to the Ultrafilter topology, when applied to elements of `α` (which are made 'pure' by the monadic `pure` operation), is the same as the original function `f`. This shows the 'extendability' of the function `f` to the Ultrafilter topology.
More concisely: For any function `f` from a type `α` to a T2 topological space `γ`, the extension of `f` to the Ultrafilter topology, composed with the `pure` operation, equals `f`.
|
denseRange_stoneCechUnit
theorem denseRange_stoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α], DenseRange stoneCechUnit
The theorem `denseRange_stoneCechUnit` states that for any type `α` that has a topology, the image of the function `stoneCechUnit` (which maps each element of `α` to its Stone-Čech compactification) is dense. This means that the set of all images of `α` in its Stone-Čech compactification is a dense set. Note that the `stoneCechUnit` function need not be an embedding, particularly when `α` is not a Hausdorff space.
More concisely: The image of the Stone-Čech compactification function is a dense subset of its domain for any topological space.
|
ultrafilter_converges_iff
theorem ultrafilter_converges_iff :
∀ {α : Type u} {u : Ultrafilter (Ultrafilter α)} {x : Ultrafilter α}, ↑u ≤ nhds x ↔ x = joinM u
This theorem states that for any given type `α`, every ultrafilter `u` on `Ultrafilter α` converges to a unique point of `Ultrafilter α`, which is `joinM u`. In other words, the ultrafilter `u` is less than or equal to the neighborhood filter of `x` if and only if `x` is equal to `joinM u`. Here, `joinM` is a function that takes a monadic value within another monadic context and combines the two contexts into one, while `nhds` is the neighborhood filter at `x` in a topological space `X`.
More concisely: For any ultrafilter `u` on a type `α`, the unique point `x` in `α` such that `nhds x ⊆ u` is equal to `joinM u`.
|
denseInducing_pure
theorem denseInducing_pure : ∀ {α : Type u}, DenseInducing pure
This theorem states that for any type `α`, the `pure` function, which maps an element of `α` to an ultrafilter of `α`, defines a dense inducing of `α` into the space of ultrafilters over `α`. In mathematical terms, this means that the image of any subset of `α` under the `pure` function is dense in the ultrafilter space over `α`. This is a fundamental property in the theory of ultrafilters and topological spaces.
More concisely: The `pure` function maps every subset of a type `α` densely into the ultrafilter space over `α`.
|
ultrafilter_extend_eq_iff
theorem ultrafilter_extend_eq_iff :
∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [inst_1 : T2Space γ] [inst_2 : CompactSpace γ] {f : α → γ}
{b : Ultrafilter α} {c : γ}, Ultrafilter.extend f b = c ↔ ↑(Ultrafilter.map f b) ≤ nhds c
This theorem states that for any types `α` and `γ`, with `γ` being a compact Hausdorff space, any function `f` from `α` to `γ`, any ultrafilter `b` on `α`, and any element `c` in `γ`, the value of the function `Ultrafilter.extend f` at the ultrafilter `b` is equal to `c` if and only if the pushforward of the ultrafilter `b` under the function `f` is less than or equal to the neighborhood filter at `c`.
In simpler terms, the value that `Ultrafilter.extend f` assigns to an ultrafilter `b` is the unique limit of the ultrafilter `b` mapped by the function `f` in the compact Hausdorff space `γ`.
More concisely: For any function `f` from a type `α` to a compact Hausdorff space `γ`, ultrafilter `b` on `α`, and element `c` in `γ`, `Ultrafilter.extend f b = c` if and only if the pushforward of `b` under `f` is contained in the neighborhood filter of `c`.
|
stoneCechExtend_extends
theorem stoneCechExtend_extends :
∀ {α : Type u} [inst : TopologicalSpace α] {γ : Type u} [inst_1 : TopologicalSpace γ] [inst_2 : T2Space γ]
[inst_3 : CompactSpace γ] {f : α → γ} (hf : Continuous f), stoneCechExtend hf ∘ stoneCechUnit = f
The theorem `stoneCechExtend_extends` states that for any type `α` with a topological space structure and any compact Hausdorff space `γ`, any continuous function `f` from `α` to `γ` can be extended to the Stone-Čech compactification of `α`. More explicitly, if we have a continuous function `f` from `α` to `γ`, then the composition of the function `stoneCechExtend` applied to `f` (which creates the extended function) with the natural map `stoneCechUnit` (which embeds `α` into its Stone-Čech compactification) is equal to `f` itself. This means that the function `f` is essentially "preserved" under this extension to the Stone-Čech compactification.
More concisely: For any continuous function from a topological space to a compact Hausdorff space, there exists an extension of the function to its Stone-Čech compactification that preserves the original function.
|
ultrafilter_isOpen_basic
theorem ultrafilter_isOpen_basic : ∀ {α : Type u} (s : Set α), IsOpen {u | s ∈ u}
The theorem `ultrafilter_isOpen_basic` states that for any type `α` and any set `s` of type `α`, the set of ultrafilters `u` such that `s` is a member of `u` is open in the topology of ultrafilters. In other words, the basic open sets for the topology on ultrafilters, which are defined as the set of ultrafilters containing a particular set, are themselves open sets.
More concisely: The set of ultrafilters containing a given set is open in the topology of ultrafilters.
|
denseEmbedding_pure
theorem denseEmbedding_pure : ∀ {α : Type u}, DenseEmbedding pure
This theorem states that for any type `α`, the function `pure`, which maps an element to an ultrafilter containing only that element, defines a dense embedding of `α` into the space of ultrafilters over `α`. That is to say, every ultrafilter over `α` can be approximated by ultrafilters that contain a single element from `α`.
More concisely: The function `pure : ∀ α, α → ultrafilter α` is a dense embedding.
|
continuous_stoneCechExtend
theorem continuous_stoneCechExtend :
∀ {α : Type u} [inst : TopologicalSpace α] {γ : Type u} [inst_1 : TopologicalSpace γ] [inst_2 : T2Space γ]
[inst_3 : CompactSpace γ] {f : α → γ} (hf : Continuous f), Continuous (stoneCechExtend hf)
The theorem `continuous_stoneCechExtend` states that for any function `f` from a topological space `α` to a compact Hausdorff space `γ`, if `f` is continuous, then the extension of `f` to the Stone-Čech compactification of `α`, denoted by `stoneCechExtend hf`, is also continuous. This extension uses the ultrafilter extension of `f`. In mathematical terms, if $\alpha$ and $\gamma$ are topological spaces, with $\gamma$ also being a compact Hausdorff space, and $f: \alpha \rightarrow \gamma$ is a continuous function, then the function extending $f$ to the Stone-Čech compactification of $\alpha$ is also a continuous function.
More concisely: If $f : \alpha \rightarrow \gamma$ is a continuous function between a topological space $\alpha$ and a compact Hausdorff space $\gamma$, then the extension of $f$ to the Stone-Čech compactification of $\alpha$ is also a continuous function.
|
ultrafilterBasis_is_basis
theorem ultrafilterBasis_is_basis : ∀ {α : Type u}, TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α)
The theorem `ultrafilterBasis_is_basis` states that for any type `α`, the `ultrafilterBasis` defined for `α` is a topological basis. In terms of topology, a topological basis is a subset of the power set of a topological space that can be used to generate the topology of that space. In this context, the sets of ultrafilters over the elements of `α` that contain a particular subset of `α` form a topological basis, meaning that every open set in the topology can be written as a union of these sets.
More concisely: The set of ultrafilters over a type `α` forms a topological basis for the Scott topology on `α`.
|
continuous_ultrafilter_extend
theorem continuous_ultrafilter_extend :
∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [inst_1 : T2Space γ] [inst_2 : CompactSpace γ]
(f : α → γ), Continuous (Ultrafilter.extend f)
The theorem `continuous_ultrafilter_extend` states that for any types `α` and `γ`, if `γ` is equipped with a topological space structure, a T2 (Hausdorff) space structure, and a compact space structure, then for any function `f` from `α` to `γ`, the extension of `f` to a function from `Ultrafilter α` to `γ` is continuous. This theorem basically establishes the continuity of the extension function when the codomain `γ` is a compact Hausdorff space.
More concisely: For any type `α` and a compact Hausdorff space `γ`, the extension of a function from `α` to `γ` to an ultrafilter on `α` is a continuous function.
|
denseRange_pure
theorem denseRange_pure : ∀ {α : Type u}, DenseRange pure
The theorem `denseRange_pure` states that for any type `α`, the range of the function `pure`, which maps from type `α` to `Ultrafilter α`, is dense in the topological space `Ultrafilter α`. In simpler terms, this means that every neighborhood in the `Ultrafilter α` space contains at least one point from the image of the `pure` function.
More concisely: The `pure` function maps `α` densely into the topological space `Ultrafilter α`.
|
induced_topology_pure
theorem induced_topology_pure : ∀ {α : Type u}, TopologicalSpace.induced pure Ultrafilter.topologicalSpace = ⊥ := by
sorry
The theorem `induced_topology_pure` states that for any type `α`, the map `pure : α → Ultrafilter α` induces the discrete topology on `α`. The discrete topology is the finest topology possible on a set, where each single point forms an open set. In other words, the map `pure` transforms the topological space structure of `Ultrafilter α` such that every subset of `α` is an open set under the induced topology.
More concisely: The map `pure : α → Ultrafilter α` induces the discrete topology on `α`.
|