isQuasiSeparated_univ_iff
theorem isQuasiSeparated_univ_iff :
∀ {α : Type u_3} [inst : TopologicalSpace α], IsQuasiSeparated Set.univ ↔ QuasiSeparatedSpace α
This theorem states that for any type α that has a topological space structure, the universal set of α (i.e., the set of all elements of α) is quasi-separated if and only if α is a quasi-separated space. Here, a set is described as quasi-separated if the intersection of any pair of compact open subsets of that set remains compact. The universal set is quasi-separated means that for any two compact open subsets, their intersection is also compact. Conversely, a quasi-separated space means the entire space has this property, so it is a generalization of the concept to the whole topological space.
More concisely: A topological space α is quasi-separated if and only if its universal set, i.e., the set of all elements in α, is quasi-separated.
|
QuasiSeparatedSpace.inter_isCompact
theorem QuasiSeparatedSpace.inter_isCompact :
∀ {α : Type u_3} [inst : TopologicalSpace α] [self : QuasiSeparatedSpace α] (U V : Set α),
IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
The theorem `QuasiSeparatedSpace.inter_isCompact` states that in any quasi-separated topological space, the intersection of two subsets that are both open and compact is also compact. More specifically, given any type `α` with a topological space structure and a quasi-separated space structure, for any two subsets `U` and `V` of `α`, if `U` and `V` are both open sets and also compact sets, then their intersection `U ∩ V` is a compact set.
More concisely: In a quasi-separated topological space, the intersection of two open and compact sets is a compact set.
|