Pointwise operations on sets in topological groups

Topological operations on pointwise sums and products

A few results about interior and closure of the pointwise addition/multiplication of sets in groups with continuous addition/multiplication. See also Submonoid.top_closure_mul_self_eq in Topology.Algebra.Monoid.

theorem subset_interior_smul {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s • interior t ⊆ interior (s • t)

theorem subset_interior_vadd {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s +ᵥ interior t ⊆ interior (s +ᵥ t)

theorem IsClosed.smul_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s • t)

If G acts on X continuously, the set s • t is closed when s : Set G is compact and t : Set X is closed.

See also IsClosed.smul_right_of_isCompact for a version with the assumptions on s and t reversed, assuming that the action is proper.

theorem IsClosed.vadd_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s +ᵥ t)

If G acts on X continuously, the set s +ᵥ t is closed when s : Set G is compact and t : Set X is closed.

See also IsClosed.vadd_right_of_isCompact for a version with the assumptions on s and t reversed, assuming that the action is proper.

theorem MulAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem AddAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem IsOpen.mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s t : Set α} : IsOpen t → IsOpen (s * t)

theorem IsOpen.add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s t : Set α} : IsOpen t → IsOpen (s + t)

theorem subset_interior_mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s t : Set α} : s * interior t ⊆ interior (s * t)

theorem subset_interior_add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s t : Set α} : s + interior t ⊆ interior (s + t)

theorem subset_interior_mul {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s t : Set α} : interior s * interior t ⊆ interior (s * t)

theorem subset_interior_add {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem singleton_mul_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : {a} * s ∈ nhds (a * b)

theorem singleton_add_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : {a} + s ∈ nhds (a + b)

theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) (h : s ∈ nhds 1) : {a} * s ∈ nhds a

theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) (h : s ∈ nhds 0) : {a} + s ∈ nhds a

theorem IsOpen.mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α} (hs : IsOpen s) : IsOpen (s * t)

theorem IsOpen.add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α} (hs : IsOpen s) : IsOpen (s + t)

theorem subset_interior_mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α} : interior s * t ⊆ interior (s * t)

theorem subset_interior_add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α} : interior s + t ⊆ interior (s + t)

theorem subset_interior_mul' {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α} : interior s * interior t ⊆ interior (s * t)

theorem subset_interior_add' {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem mul_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : s * {a} ∈ nhds (b * a)

theorem add_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s ∈ nhds b) : s + {a} ∈ nhds (b + a)

theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) (h : s ∈ nhds 1) : s * {a} ∈ nhds a

theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) (h : s ∈ nhds 0) : s + {a} ∈ nhds a

theorem closure_subset_mul_left_of_mem_nhds_one_of_inv {G : Type w} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {s : Set G} (s' : Set G) (hs₀ : s ∈ nhds 1) (h_symm : ∀ x ∈ s, x⁻¹ ∈ s) : closure s' ⊆ s * s'

theorem closure_subset_add_left_of_mem_nhds_zero_of_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {s : Set G} (s' : Set G) (hs₀ : s ∈ nhds 0) (h_symm : ∀ x ∈ s, -x ∈ s) : closure s' ⊆ s + s'

theorem closure_subset_mul_right_of_mem_nhds_one_of_inv {G : Type w} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (s : Set G) {s' : Set G} (hs'₀ : s' ∈ nhds 1) (h_symm : ∀ x ∈ s', x⁻¹ ∈ s') : closure s ⊆ s * s'

theorem closure_subset_add_right_of_mem_nhds_zero_of_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (s : Set G) {s' : Set G} (hs'₀ : s' ∈ nhds 0) (h_symm : ∀ x ∈ s', -x ∈ s') : closure s ⊆ s + s'

theorem closure_subset_of_mem_nhds_one_of_inv_mul_left_subset {G : Type w} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {s s' t : Set G} (hs₀ : s ∈ nhds 1) (h_symm : ∀ x ∈ s, x⁻¹ ∈ s) (hs : s * s' ⊆ t) : closure s' ⊆ t

theorem closure_subset_of_mem_nhds_zero_of_neg_add_left_subset {G : Type w} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {s s' t : Set G} (hs₀ : s ∈ nhds 0) (h_symm : ∀ x ∈ s, -x ∈ s) (hs : s + s' ⊆ t) : closure s' ⊆ t

theorem closure_subset_of_mem_nhds_one_of_inv_mul_right_subset {G : Type w} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {s s' t : Set G} (hs'₀ : s' ∈ nhds 1) (h_symm : ∀ x ∈ s', x⁻¹ ∈ s') (hs : s * s' ⊆ t) : closure s ⊆ t

theorem closure_subset_of_mem_nhds_zero_of_neg_add_right_subset {G : Type w} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {s s' t : Set G} (hs'₀ : s' ∈ nhds 0) (h_symm : ∀ x ∈ s', -x ∈ s') (hs : s + s' ⊆ t) : closure s ⊆ t

theorem IsOpen.div_left {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (ht : IsOpen t) : IsOpen (s / t)

theorem IsOpen.sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsOpen t) : IsOpen (s - t)

theorem IsOpen.div_right {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (hs : IsOpen s) : IsOpen (s / t)

theorem IsOpen.sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (hs : IsOpen s) : IsOpen (s - t)

theorem subset_interior_div_left {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} : interior s / t ⊆ interior (s / t)

theorem subset_interior_sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : interior s - t ⊆ interior (s - t)

theorem subset_interior_div_right {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} : s / interior t ⊆ interior (s / t)

theorem subset_interior_sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : s - interior t ⊆ interior (s - t)

theorem subset_interior_div {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} : interior s / interior t ⊆ interior (s / t)

theorem subset_interior_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : interior s - interior t ⊆ interior (s - t)

theorem IsOpen.mul_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s * closure t = s * t

theorem IsOpen.add_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s + closure t = s + t

theorem IsOpen.closure_mul {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s * t = s * t

theorem IsOpen.closure_add {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s + t = s + t

theorem IsOpen.div_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s / closure t = s / t

theorem IsOpen.sub_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s - closure t = s - t

theorem IsOpen.closure_div {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s / t = s / t

theorem IsOpen.closure_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s - t = s - t

theorem IsClosed.mul_left_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s * t)

theorem IsClosed.add_left_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s + t)

theorem IsClosed.mul_right_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t * s)

theorem IsClosed.add_right_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t + s)

theorem subset_mul_closure_one {G : Type u_1} [MulOneClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s * closure {1}

theorem subset_add_closure_zero {G : Type u_1} [AddZeroClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s + closure {0}

theorem IsCompact.mul_closure_one_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {K : Set G} (hK : IsCompact K) : K * closure {1} = closure K

theorem IsCompact.add_closure_zero_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) : K + closure {0} = closure K

theorem IsClosed.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {F : Set G} (hF : IsClosed F) : F * closure {1} = F

theorem IsClosed.add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Set G} (hF : IsClosed F) : F + closure {0} = F

theorem compl_mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} (ht : t * closure {1} = t) : tᶜ * closure {1} = tᶜ

theorem compl_add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : t + closure {0} = t) : tᶜ + closure {0} = tᶜ

theorem compl_mul_closure_one_eq_iff {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {t : Set G} : tᶜ * closure {1} = tᶜ ↔ t * closure {1} = t

theorem compl_add_closure_zero_eq_iff {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} : tᶜ + closure {0} = tᶜ ↔ t + closure {0} = t

theorem IsOpen.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {U : Set G} (hU : IsOpen U) : U * closure {1} = U

theorem IsOpen.add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : IsOpen U) : U + closure {0} = U

theorem closure_subset_mul_right_of_mem_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {V : Set G} (U : Set G) (hV : V ∈ nhds 1) : closure U ⊆ U * V

theorem closure_subset_add_right_of_mem_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {V : Set G} (U : Set G) (hV : V ∈ nhds 0) : closure U ⊆ U + V

theorem closure_subset_mul_left_of_mem_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {U : Set G} (V : Set G) (hU : U ∈ nhds 1) : closure V ⊆ U * V

theorem closure_subset_add_left_of_mem_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (V : Set G) (hU : U ∈ nhds 0) : closure V ⊆ U + V

theorem closure_subset_mul_self_of_mem_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {U : Set G} (hU : U ∈ nhds 1) : closure U ⊆ U * U

theorem closure_subset_add_self_of_mem_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : U ∈ nhds 0) : closure U ⊆ U + U

theorem Filter.HasBasis.iInter_mul_right_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), s * U i = closure s

In a topological group, the closure of a set s is the intersection of s * U where U ranges over any basis of 𝓝 1. Note that s * U does not constitute a basis of 𝓝ˢ s

theorem Filter.HasBasis.iInter_add_right_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), s + U i = closure s

In a topological additive group, the closure of a set s is the intersection of s + U where U ranges over any basis of 𝓝 0. Note that s + U does not constitute a basis of 𝓝ˢ s

theorem Filter.HasBasis.iInter_mul_left_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), U i * s = closure s

In a topological group, the closure of a set s is the intersection of U * s where U ranges over any basis of 𝓝 1. Note that U * s does not constitute a basis of 𝓝ˢ s

theorem Filter.HasBasis.iInter_add_left_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), U i + s = closure s

In a topological additive group, the closure of a set s is the intersection of U + s where U ranges over any basis of 𝓝 0. Note that U + s does not constitute a basis of 𝓝ˢ s

theorem Filter.HasBasis.iInter_closure_mul_right_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (s * U i) = closure s

In a topological group, the closure of a set s is the intersection of closure (s * U) where U ranges over any basis of 𝓝 1.

theorem Filter.HasBasis.iInter_closure_add_right_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (s + U i) = closure s

In a topological additive group, the closure of a set s is the intersection of closure (s + U) where U ranges over any basis of 𝓝 0.

theorem Filter.HasBasis.iInter_closure_mul_left_eq_closure {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (U i * s) = closure s

In a topological group, the closure of a set s is the intersection of closure (U * s) where U ranges over any basis of 𝓝 1.

theorem Filter.HasBasis.iInter_closure_add_left_eq_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (U i + s) = closure s

In a topological additive group, the closure of a set s is the intersection of closure (U + s) where U ranges over any basis of 𝓝 0.

theorem IsClosed.iInter_closure_mul_right_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Type u_1} {s : Set G} (hs : IsClosed s) {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (s * U i) = s

theorem IsClosed.iInter_closure_add_right_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} (hs : IsClosed s) {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (s + U i) = s

theorem IsClosed.iInter_closure_mul_left_eq {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {ι : Type u_1} {s : Set G} (hs : IsClosed s) {p : ι → Prop} {U : ι → Set G} (hU : (nhds 1).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (U i * s) = s

theorem IsClosed.iInter_closure_add_left_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} (hs : IsClosed s) {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ (i : ι), ⋂ (_ : p i), closure (U i + s) = s

@[instance 100]

instance IsTopologicalGroup.regularSpace (G : Type w) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : RegularSpace G

@[instance 100]

instance IsTopologicalAddGroup.regularSpace (G : Type w) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : RegularSpace G

theorem group_inseparable_iff {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {x y : G} : Inseparable x y ↔ x / y ∈ closure 1

theorem addGroup_inseparable_iff {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {x y : G} : Inseparable x y ↔ x - y ∈ closure 0

theorem IsTopologicalGroup.t2Space_iff_one_closed {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : T2Space G ↔ IsClosed {1}

theorem IsTopologicalAddGroup.t2Space_iff_zero_closed {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : T2Space G ↔ IsClosed {0}

theorem IsTopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (H : ∀ (x : G), x ≠ 1 → ∃ U ∈ nhds 1, x ∉ U) : T2Space G

theorem IsTopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (H : ∀ (x : G), x ≠ 0 → ∃ U ∈ nhds 0, x ∉ U) : T2Space G

theorem exists_closed_nhds_one_inv_eq_mul_subset {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {U : Set G} (hU : U ∈ nhds 1) : ∃ V ∈ nhds 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V * V ⊆ U.

theorem exists_closed_nhds_zero_neg_eq_add_subset {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : U ∈ nhds 0) : ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U

Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V + V ⊆ U.

theorem IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) (hS : IsDiscrete ↑S) : ∃ U ∈ nhds 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) => g * x) '' U ∩ U).Nonempty → g = 1

theorem IsDiscrete.exists_nhds_eq_zero_of_image_addLeft_inter_nonempty {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : IsDiscrete ↑S) : ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun (x : G) => g + x) '' U ∩ U).Nonempty → g = 0

theorem IsDiscrete.exists_nhds_eq_one_of_image_mulRight_inter_nonempty {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) (hS : IsDiscrete ↑S) : ∃ U ∈ nhds 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) => x * g) '' U ∩ U).Nonempty → g = 1

theorem IsDiscrete.exists_nhds_eq_zero_of_image_addRight_inter_nonempty {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : IsDiscrete ↑S) : ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun (x : G) => x + g) '' U ∩ U).Nonempty → g = 0

theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {G : Type w} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G

If a point in a topological group has a compact neighborhood, then the group is locally compact.

theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G

theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological additive group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has compact support, then either the function is trivial or the group is locally compact.

theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological additive group has compact support, then either the function is trivial or the group is locally compact.