Compactum.str_eq_of_le_nhds
theorem Compactum.str_eq_of_le_nhds : ∀ {X : Compactum} (F : Ultrafilter X.A) (x : X.A), ↑F ≤ nhds x → X.str F = x := by
sorry
This theorem states that for any compactum `X`, given an ultrafilter `F` on `X.A` and an element `x` of `X.A`, if `F` is less than or equal to the neighborhood filter at `x`, then the structure map of `X` applied to `F` equals `x`. In other words, if the ultrafilter `F` is within the neighborhood of `x`, then the limit of the ultrafilter, as evaluated by the structure map, is `x` itself.
More concisely: For any compactum X and ultrafilter F on X.A, if F is contained in the neighborhood filter of x in X.A, then the limit of F, under the structure map of X, is x.
|
Compactum.le_nhds_of_str_eq
theorem Compactum.le_nhds_of_str_eq : ∀ {X : Compactum} (F : Ultrafilter X.A) (x : X.A), X.str F = x → ↑F ≤ nhds x := by
sorry
This theorem states that for any compactum `X`, ultrafilter `F` on the algebra `X.A`, and an element `x` in the algebra `X.A`, if the structure map of the compactum applied to `F` equals `x`, then the ultrafilter `F` is less than or equal to the neighborhood filter at `x`. In more conventional terms, this means that if an ultrafilter's limit point in a compactum is `x`, then all elements of the ultrafilter are in the neighborhood of `x`. This aligns with the intuition that an ultrafilter should 'converge' to its limit point in a topological sense, in this case meaning that all its elements are close to `x` in the sense of being in its topological neighborhood.
More concisely: For any compactum X, if the structure map of X applied to an ultrafilter F equals an element x in X.A, then F is contained in the neighborhood filter of x.
|
Compactum.lim_eq_str
theorem Compactum.lim_eq_str : ∀ {X : Compactum} (F : Ultrafilter X.A), F.lim = X.str F
The theorem `Compactum.lim_eq_str` asserts that for any compactum `X` and any ultrafilter `F` on `X.A` (the underlying set of `X`), the limit of `F` (`F.lim`) is equal to the structure map (`X.str`) applied to `F`. In other words, the structure map of a compactum precisely computes the limits of ultrafilters on its underlying set.
More concisely: For any compactum X and ultrafilter F on X.A, the limit of F equals the application of X.str to F.
|
Compactum.continuous_of_hom
theorem Compactum.continuous_of_hom : ∀ {X Y : Compactum} (f : X ⟶ Y), Continuous f.f
This theorem states that any morphism of compacta is continuous. In other words, if `X` and `Y` are both compacta (as defined in the type `Compactum`), and `f` is a morphism from `X` to `Y`, then `f` is a continuous function. This is a statement about the category of compacta, which are defined as algebras for the ultrafilter monad in Lean 4.
More concisely: If `X` and `Y` are compact topological spaces and `f : X → Y` is a morphism (in the category-theoretic sense), then `f` is a continuous function.
|