Basic results on topological groups

This file develops general consequences of the topological-group axioms. It includes the homeomorphisms given by left and right multiplication, continuity of conjugation, induced and product topological-group structures, and results about compact sets and connected components.

It also constructs infima of topological-group topologies. Results specifically about inversion, division, neighbourhoods, integer powers, ordered groups, subgroups, and units are provided by the corresponding sibling files.

Tags

topological space, group, topological group

theorem Set.isClosed_centralizer {M : Type u_5} (s : Set M) [Mul M] [TopologicalSpace M] [SeparatelyContinuousMul M] [T2Space M] : IsClosed s.centralizer

In a Hausdorff magma with continuous multiplication, the centralizer of any set is closed.

Groups with continuous multiplication

In this section we prove a few statements about groups with continuous (*).

def Homeomorph.mulLeft {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : G ≃ₜ G

Multiplication from the left in a topological group as a homeomorphism.

Equations

• Homeomorph.mulLeft a = { toEquiv := Equiv.mulLeft a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.addLeft {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : G ≃ₜ G

Addition from the left in a topological additive group as a homeomorphism.

Equations

• Homeomorph.addLeft a = { toEquiv := Equiv.addLeft a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.coe_mulLeft {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : ⇑(Homeomorph.mulLeft a) = fun (x : G) => a * x

@[simp]

theorem Homeomorph.coe_addLeft {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : ⇑(Homeomorph.addLeft a) = fun (x : G) => a + x

theorem Homeomorph.mulLeft_symm {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

theorem Homeomorph.addLeft_symm {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : (Homeomorph.addLeft a).symm = Homeomorph.addLeft (-a)

theorem isOpenMap_mul_left {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : IsOpenMap fun (x : G) => a * x

theorem isOpenMap_add_left {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : IsOpenMap fun (x : G) => a + x

theorem IsOpen.leftCoset {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (x • U)

theorem IsOpen.left_addCoset {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (x +ᵥ U)

theorem isClosedMap_mul_left {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : IsClosedMap fun (x : G) => a * x

theorem isClosedMap_add_left {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : IsClosedMap fun (x : G) => a + x

theorem IsClosed.leftCoset {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (x • U)

theorem IsClosed.left_addCoset {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (x +ᵥ U)

@[simp]

theorem Filter.map_mul_left_nhdsNE {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {c a : G} : map (fun (x : G) => c * x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c * a) {c * a}ᶜ

@[simp]

theorem Filter.map_add_left_nhdsNE {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {c a : G} : map (fun (x : G) => c + x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c + a) {c + a}ᶜ

def Homeomorph.mulRight {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : G ≃ₜ G

Multiplication from the right in a topological group as a homeomorphism.

Equations

• Homeomorph.mulRight a = { toEquiv := Equiv.mulRight a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.addRight {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : G ≃ₜ G

Addition from the right in a topological additive group as a homeomorphism.

Equations

• Homeomorph.addRight a = { toEquiv := Equiv.addRight a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.coe_mulRight {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : ⇑(Homeomorph.mulRight a) = fun (x : G) => x * a

@[simp]

theorem Homeomorph.coe_addRight {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : ⇑(Homeomorph.addRight a) = fun (x : G) => x + a

theorem Homeomorph.mulRight_symm {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

theorem Homeomorph.addRight_symm {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : (Homeomorph.addRight a).symm = Homeomorph.addRight (-a)

theorem isOpenMap_mul_right {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : IsOpenMap fun (x : G) => x * a

theorem isOpenMap_add_right {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : IsOpenMap fun (x : G) => x + a

theorem IsOpen.rightCoset {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (MulOpposite.op x • U)

theorem IsOpen.right_addCoset {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (AddOpposite.op x +ᵥ U)

theorem isClosedMap_mul_right {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (a : G) : IsClosedMap fun (x : G) => x * a

theorem isClosedMap_add_right {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (a : G) : IsClosedMap fun (x : G) => x + a

theorem IsClosed.rightCoset {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (MulOpposite.op x • U)

theorem IsClosed.right_addCoset {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (AddOpposite.op x +ᵥ U)

@[simp]

theorem Filter.map_mul_right_nhdsNE {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {c a : G} : map (fun (x : G) => x * c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a * c) {a * c}ᶜ

@[simp]

theorem Filter.map_add_right_nhdsNE {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {c a : G} : map (fun (x : G) => x + c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a + c) {a + c}ᶜ

theorem discreteTopology_iff_isOpen_singleton_one {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] : DiscreteTopology G ↔ IsOpen {1}

theorem discreteTopology_iff_isOpen_singleton_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] : DiscreteTopology G ↔ IsOpen {0}

theorem discreteTopology_of_isOpen_singleton_one {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (h : IsOpen {1}) : DiscreteTopology G

theorem discreteTopology_of_isOpen_singleton_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (h : IsOpen {0}) : DiscreteTopology G

theorem smul_connectedComponent {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (g h : G) : g • connectedComponent h = connectedComponent (g * h)

theorem vadd_connectedComponent {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (g h : G) : g +ᵥ connectedComponent h = connectedComponent (g + h)

theorem totallyDisconnectedSpace_iff_connectedComponent_one {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] : TotallyDisconnectedSpace G ↔ connectedComponent 1 = {1}

theorem totallyDisconnectedSpace_iff_connectedComponent_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] : TotallyDisconnectedSpace G ↔ connectedComponent 0 = {0}

theorem Filter.tendsto_mul_const_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (x : α) => f x * b) l (nhds (c * b)) ↔ Tendsto f l (nhds c)

theorem Filter.tendsto_add_const_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (x : α) => f x + b) l (nhds (c + b)) ↔ Tendsto f l (nhds c)

theorem Filter.tendsto_const_mul_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (x : α) => b * f x) l (nhds (b * c)) ↔ Tendsto f l (nhds c)

theorem Filter.tendsto_const_add_iff {G : Type u_1} {α : Type u_3} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (x : α) => b + f x) l (nhds (b + c)) ↔ Tendsto f l (nhds c)

Topological groups

A topological group is a group in which the multiplication and inversion operations are continuous. Topological additive groups are defined in the same way. Equivalently, we can require that the division operation x y ↦ x * y⁻¹ (resp., subtraction) is continuous.

instance ConjAct.units_continuousConstSMul {M : Type u_5} [Monoid M] [TopologicalSpace M] [ContinuousMul M] : ContinuousConstSMul (ConjAct Mˣ) M

instance instDiscreteTopologySubtypeMemSubgroupHSMulOfContinuousConstSMul {G : Type u_1} {H : Type u_2} [Group G] [Group H] [TopologicalSpace G] [MulDistribMulAction H G] [ContinuousConstSMul H G] {𝒢 : Subgroup G} (h : H) [DiscreteTopology ↥𝒢] : DiscreteTopology ↥(h • 𝒢)

theorem IsTopologicalGroup.continuous_conj_prod {G : Type u_1} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] [ContinuousInv G] : Continuous fun (g : G × G) => g.1 * g.2 * g.1⁻¹

Conjugation is jointly continuous on G × G when both mul and inv are continuous.

theorem IsTopologicalAddGroup.continuous_addConj_prod {G : Type u_1} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] [ContinuousNeg G] : Continuous fun (g : G × G) => g.1 + g.2 + -g.1

Conjugation is jointly continuous on G × G when both add and neg are continuous.

theorem IsTopologicalGroup.continuous_conj {G : Type u_1} [TopologicalSpace G] [Inv G] [Mul G] [SeparatelyContinuousMul G] (g : G) : Continuous fun (h : G) => g * h * g⁻¹

Conjugation by a fixed element is continuous when mul is continuous.

theorem IsTopologicalAddGroup.continuous_addConj {G : Type u_1} [TopologicalSpace G] [Neg G] [Add G] [SeparatelyContinuousAdd G] (g : G) : Continuous fun (h : G) => g + h + -g

Conjugation by a fixed element is continuous when add is continuous.

instance instContinuousConstSMulConjActOfSeparatelyContinuousMul {G : Type u_5} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : ContinuousConstSMul (ConjAct G) G

theorem IsTopologicalGroup.continuous_conj' {G : Type u_1} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] [ContinuousInv G] (h : G) : Continuous fun (g : G) => g * h * g⁻¹

Conjugation acting on fixed element of the group is continuous when both mul and inv are continuous.

theorem IsTopologicalAddGroup.continuous_addConj' {G : Type u_1} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] [ContinuousNeg G] (h : G) : Continuous fun (g : G) => g + h + -g

Conjugation acting on fixed element of the additive group is continuous when both add and neg are continuous.

instance instIsTopologicalGroupULift {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalGroup (ULift.{u_5, u_1} G)

instance Prod.instIsTopologicalGroup {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace H] [Group H] [IsTopologicalGroup H] : IsTopologicalGroup (G × H)

instance Prod.instIsTopologicalAddGroup {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace H] [AddGroup H] [IsTopologicalAddGroup H] : IsTopologicalAddGroup (G × H)

instance OrderDual.instIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalGroup Gᵒᵈ

instance OrderDual.instIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalAddGroup Gᵒᵈ

instance Pi.topologicalGroup {β : Type u_4} {C : β → Type u_5} [(b : β) → TopologicalSpace (C b)] [(b : β) → Group (C b)] [∀ (b : β), IsTopologicalGroup (C b)] : IsTopologicalGroup ((b : β) → C b)

instance Pi.topologicalAddGroup {β : Type u_4} {C : β → Type u_5} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), IsTopologicalAddGroup (C b)] : IsTopologicalAddGroup ((b : β) → C b)

instance instContinuousInvMulOpposite {α : Type u_3} [TopologicalSpace α] [Inv α] [ContinuousInv α] : ContinuousInv αᵐᵒᵖ

instance instContinuousNegAddOpposite {α : Type u_3} [TopologicalSpace α] [Neg α] [ContinuousNeg α] : ContinuousNeg αᵃᵒᵖ

instance instIsTopologicalGroupMulOpposite {α : Type u_3} [TopologicalSpace α] [Group α] [IsTopologicalGroup α] : IsTopologicalGroup αᵐᵒᵖ

If multiplication is continuous in α, then it also is in αᵐᵒᵖ.

instance instIsTopologicalAddGroupAddOpposite {α : Type u_3} [TopologicalSpace α] [AddGroup α] [IsTopologicalAddGroup α] : IsTopologicalAddGroup αᵃᵒᵖ

If addition is continuous in α, then it also is in αᵃᵒᵖ.

theorem nhds_one_symm (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Filter.comap Inv.inv (nhds 1) = nhds 1

theorem nhds_zero_symm (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : Filter.comap Neg.neg (nhds 0) = nhds 0

theorem nhds_one_symm' (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Filter.map Inv.inv (nhds 1) = nhds 1

theorem nhds_zero_symm' (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : Filter.map Neg.neg (nhds 0) = nhds 0

theorem inv_mem_nhds_one (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {S : Set G} (hS : S ∈ nhds 1) : S⁻¹ ∈ nhds 1

theorem neg_mem_nhds_zero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {S : Set G} (hS : S ∈ nhds 0) : -S ∈ nhds 0

def Homeomorph.shearMulRight (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : G × G ≃ₜ G × G

The map (x, y) ↦ (x, x * y) as a homeomorphism. This is a shear mapping.

Equations

• Homeomorph.shearMulRight G = { toEquiv := (Equiv.refl G).prodShear Equiv.mulLeft, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.shearAddRight (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : G × G ≃ₜ G × G

The map (x, y) ↦ (x, x + y) as a homeomorphism. This is a shear mapping.

Equations

• Homeomorph.shearAddRight G = { toEquiv := (Equiv.refl G).prodShear Equiv.addLeft, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.shearMulRight_coe (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ⇑(Homeomorph.shearMulRight G) = fun (z : G × G) => (z.1, z.1 * z.2)

@[simp]

theorem Homeomorph.shearAddRight_coe (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ⇑(Homeomorph.shearAddRight G) = fun (z : G × G) => (z.1, z.1 + z.2)

@[simp]

theorem Homeomorph.shearMulRight_symm_coe (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ⇑(Homeomorph.shearMulRight G).symm = fun (z : G × G) => (z.1, z.1⁻¹ * z.2)

@[simp]

theorem Homeomorph.shearAddRight_symm_coe (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ⇑(Homeomorph.shearAddRight G).symm = fun (z : G × G) => (z.1, -z.1 + z.2)

theorem Topology.IsInducing.topologicalGroup {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {F : Type u_5} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : IsInducing ⇑f) : IsTopologicalGroup H

theorem Topology.IsInducing.topologicalAddGroup {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Type u_5} [AddGroup H] [TopologicalSpace H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) (hf : IsInducing ⇑f) : IsTopologicalAddGroup H

theorem topologicalGroup_induced {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {F : Type u_5} [Group H] [FunLike F H G] [MonoidHomClass F H G] (f : F) : IsTopologicalGroup H

theorem topologicalAddGroup_induced {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Type u_5} [AddGroup H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) : IsTopologicalAddGroup H

theorem IsTopologicalGroup.t1Space (G : Type u_1) [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsClosed {1}) : T1Space G

theorem IsTopologicalAddGroup.t1Space (G : Type u_1) [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (h : IsClosed {0}) : T1Space G

Some results about an open set containing the product of two sets in a topological group.

theorem compact_open_separated_mul_right {G : Type u_1} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ nhds 1, K * V ⊆ U

Given a compact set K inside an open set U, there is an open neighborhood V of 1 such that K * V ⊆ U.

theorem compact_open_separated_add_right {G : Type u_1} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ nhds 0, K + V ⊆ U

Given a compact set K inside an open set U, there is an open neighborhood V of 0 such that K + V ⊆ U.

theorem compact_open_separated_mul_left {G : Type u_1} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ nhds 1, V * K ⊆ U

Given a compact set K inside an open set U, there is an open neighborhood V of 1 such that V * K ⊆ U.

theorem compact_open_separated_add_left {G : Type u_1} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ nhds 0, V + K ⊆ U

Given a compact set K inside an open set U, there is an open neighborhood V of 0 such that V + K ⊆ U.

theorem compact_covered_by_mul_left_translates {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) : ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) => g * x) ⁻¹' V

A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.

theorem compact_covered_by_add_left_translates {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) : ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (x : G) => g + x) ⁻¹' V

A compact set is covered by finitely many left additive translates of a set with non-empty interior.

@[instance 100]

instance SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

Every weakly locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

@[instance 100]

instance SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

Every weakly locally compact separable topological additive group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

theorem exists_disjoint_smul_of_isCompact {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [NoncompactSpace G] {K L : Set G} (hK : IsCompact K) (hL : IsCompact L) : ∃ (g : G), Disjoint K (g • L)

Given two compact sets in a noncompact topological group, there is a translate of the second one that is disjoint from the first one.

theorem exists_disjoint_vadd_of_isCompact {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [NoncompactSpace G] {K L : Set G} (hK : IsCompact K) (hL : IsCompact L) : ∃ (g : G), Disjoint K (g +ᵥ L)

Given two compact sets in a noncompact additive topological group, there is a translate of the second one that is disjoint from the first one.

instance instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup {G : Type u_5} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalAddGroup (Additive G)

instance instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup {G : Type u_5} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalGroup (Multiplicative G)

theorem topologicalGroup_sInf {G : Type u_1} [Group G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, IsTopologicalGroup G) : IsTopologicalGroup G

theorem topologicalAddGroup_sInf {G : Type u_1} [AddGroup G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, IsTopologicalAddGroup G) : IsTopologicalAddGroup G

theorem topologicalGroup_iInf {G : Type u_1} {ι : Sort u_5} [Group G] {ts' : ι → TopologicalSpace G} (h' : ∀ (i : ι), IsTopologicalGroup G) : IsTopologicalGroup G

theorem topologicalAddGroup_iInf {G : Type u_1} {ι : Sort u_5} [AddGroup G] {ts' : ι → TopologicalSpace G} (h' : ∀ (i : ι), IsTopologicalAddGroup G) : IsTopologicalAddGroup G

theorem topologicalGroup_inf {G : Type u_1} [Group G] {t₁ t₂ : TopologicalSpace G} (h₁ : IsTopologicalGroup G) (h₂ : IsTopologicalGroup G) : IsTopologicalGroup G

theorem topologicalAddGroup_inf {G : Type u_1} [AddGroup G] {t₁ t₂ : TopologicalSpace G} (h₁ : IsTopologicalAddGroup G) (h₂ : IsTopologicalAddGroup G) : IsTopologicalAddGroup G