IsClosed.tendsto_coe_cofinite_of_discreteTopology
theorem IsClosed.tendsto_coe_cofinite_of_discreteTopology :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
IsClosed s → DiscreteTopology ↑s → Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X)
The theorem `IsClosed.tendsto_coe_cofinite_of_discreteTopology` states that for any type `X` equipped with a topological space structure, and any set `s` in `X`, if `s` is a closed set and the induced topology on `s` is discrete, then the natural function that sends an element of `s` to the same element in `X` (termed `Subtype.val`) is a function that tends to pull back complements of compact sets (termed `Filter.cocompact X`) to subsets whose complements are finite (termed `Filter.cofinite`). In other words, for every open set in `X` whose complement is compact, the preimage of that set under the function `Subtype.val` is an open set in `s` whose complement is finite. This is a generalization of the fact that in a discrete space, every set is open, and hence, closed, and in finite sets, every filter converges.
More concisely: Given a topological space `(X : Type)` and a closed subset `s : X`, if the topology on `s` is discrete, then the inclusion map `s ↪ X` is continuous and sends compact sets to cofinite sets.
|
isClosed_and_discrete_iff
theorem isClosed_and_discrete_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X},
IsClosed S ∧ DiscreteTopology ↑S ↔ ∀ (x : X), Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal S)
This theorem provides a criterion for a subset `S` of a topological space `X` to be both closed and discrete. The criterion is in terms of the punctured neighborhood filter at any arbitrary point `x` of `X`. Specifically, `S` is closed and discrete if and only if the filter of all neighborhoods of `x` that are also within the complement of `{x}` is disjoint from the filter of all supersets of `S`. This is a generalization of the concept of a discrete topology where each point forms an isolated set.
More concisely: A subset S of a topological space X is closed and discrete if and only if the filter of neighborhoods of any x in X that are contained in the complement of {x} is disjoint from the filter of supersets of S.
|