AnabelianGeometry.CuspidalInertia.exists_openNormal_separates_compact
One open normal quotient separates two entire disjoint compact sets.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.CuspidalInertia
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]Lean source · statement
theorem exists_openNormal_separates_compact {S T : Set G}
(hS : IsCompact S) (hT : IsCompact T) (hd : Disjoint S T) :
∃ U : OpenNormalSubgroup G, ∀ s ∈ S, ∀ t ∈ T,
QuotientGroup.mk' (U : Subgroup G) s ≠ QuotientGroup.mk' (U : Subgroup G) t