Mathlib.Topology.Algebra.Group.Pointwise

subset_interior_smul theorem

: interior s • interior t ⊆ interior (s • t)

Full source

@[to_additive]
theorem subset_interior_smul : interiorinterior s • interior t ⊆ interior (s • t) :=
  (Set.smul_subset_smul_right interior_subset).trans subset_interior_smul_right

Interior of Product Contains Product of Interiors in Topological Groups

Informal description

For any subsets $s$ and $t$ of a topological group $G$, the product of their interiors is contained in the interior of their product, i.e., $\text{interior}(s) \cdot \text{interior}(t) \subseteq \text{interior}(s \cdot t)$.

IsClosed.smul_left_of_isCompact theorem

(ht : IsClosed t) (hs : IsCompact s) : IsClosed (s • t)

Full source

@[to_additive]
theorem IsClosed.smul_left_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
    IsClosed (s • t) := by
  have : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t := by
    rintro x ⟨g, hgs, y, hyt, rfl⟩
    refine ⟨g, hgs, ?_⟩
    rwa [inv_smul_smul]
  choose! f hf using this
  refine isClosed_of_closure_subset (fun x hx ↦ ?_)
  rcases mem_closure_iff_ultrafilter.mp hx with ⟨u, hust, hux⟩
  have : Ultrafilter.map f u ≤ 𝓟 s :=
    calc Ultrafilter.map f u ≤ map f (𝓟 (s • t)) := map_mono (le_principal_iff.mpr hust)
      _ = 𝓟 (f '' (s • t)) := map_principal
      _ ≤ 𝓟 s := principal_mono.mpr (image_subset_iff.mpr (fun x hx ↦ (hf x hx).1))
  rcases hs.ultrafilter_le_nhds (Ultrafilter.map f u) this with ⟨g, hg, hug⟩
  suffices g⁻¹g⁻¹ • x ∈ t from
    ⟨g, hg, g⁻¹ • x, this, smul_inv_smul _ _⟩
  exact ht.mem_of_tendsto ((Tendsto.inv hug).smul hux)
    (Eventually.mono hust (fun y hy ↦ (hf y hy).2))

Closedness of compact-closed product in topological groups

Informal description

Let $G$ be a topological group with continuous scalar multiplication, and let $s, t \subseteq G$ be subsets. If $s$ is compact and $t$ is closed, then their pointwise product $s \cdot t$ is closed in $G$.

MulAction.isClosedMap_quotient theorem

 [CompactSpace α] :
  letI := orbitRel α β
  IsClosedMap (Quotient.mk' : β → Quotient (orbitRel α β))

Full source

@[to_additive]
theorem MulAction.isClosedMap_quotient [CompactSpace α] :
    letI := orbitRel α β
    IsClosedMap (Quotient.mk' : β → Quotient (orbitRel α β)) := by
  intro t ht
  rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
    MulAction.quotient_preimage_image_eq_union_mul]
  convert ht.smul_left_of_isCompact (isCompact_univ (X := α))
  rw [← biUnion_univ, ← iUnion_smul_left_image]
  simp only [image_smul]

Closedness of the quotient map for group actions on compact spaces

Informal description

Let $G$ be a group acting continuously on a compact topological space $X$. Then the quotient map $\pi \colon X \to X/G$ is a closed map, where $X/G$ is the orbit space of the action equipped with the quotient topology.

IsOpen.mul_left theorem

: IsOpen t → IsOpen (s * t)

Full source

@[to_additive]
theorem IsOpen.mul_left : IsOpen t → IsOpen (s * t) :=
  IsOpen.smul_left

Openness of Left Multiplication by a Set in a Topological Group

Informal description

Let $G$ be a group with a topological space structure, and let $s$ be any subset of $G$. If $t$ is an open subset of $G$, then the product set $s \cdot t$ is also open in $G$.

subset_interior_mul_right theorem

: s * interior t ⊆ interior (s * t)

Full source

@[to_additive]
theorem subset_interior_mul_right : s * interior t ⊆ interior (s * t) :=
  subset_interior_smul_right

Inclusion of product with interior in interior of product

Informal description

For any subsets $s$ and $t$ of a topological group $G$, the product of $s$ with the interior of $t$ is contained in the interior of the product $s \cdot t$, i.e., $s \cdot \text{int}(t) \subseteq \text{int}(s \cdot t)$.

subset_interior_mul theorem

: interior s * interior t ⊆ interior (s * t)

Full source

@[to_additive]
theorem subset_interior_mul : interiorinterior s * interior t ⊆ interior (s * t) :=
  subset_interior_smul

Interior of product contains product of interiors in topological groups

Informal description

For any subsets $s$ and $t$ of a topological group $G$, the product of their interiors is contained in the interior of their product, i.e., $\text{int}(s) \cdot \text{int}(t) \subseteq \text{int}(s \cdot t)$.

singleton_mul_mem_nhds theorem

(a : α) {b : α} (h : s ∈ 𝓝 b) : { a } * s ∈ 𝓝 (a * b)

Full source

@[to_additive]
theorem singleton_mul_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : {a}{a} * s ∈ 𝓝 (a * b) := by
  rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]

Neighborhood of product under left multiplication: $\{a\} \cdot s \in \mathcal{N}(a \cdot b)$

Informal description

For any elements $a$ and $b$ in a topological group $\alpha$, if a set $s$ is a neighborhood of $b$, then the set $\{a\} \cdot s$ is a neighborhood of $a \cdot b$.

singleton_mul_mem_nhds_of_nhds_one theorem

(a : α) (h : s ∈ 𝓝 (1 : α)) : { a } * s ∈ 𝓝 a

Full source

@[to_additive]
theorem singleton_mul_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : {a}{a} * s ∈ 𝓝 a := by
  simpa only [mul_one] using singleton_mul_mem_nhds a h

Neighborhood of $a$ under left multiplication by a neighborhood of the identity

Informal description

Let $\alpha$ be a topological group with identity element $1$. For any element $a \in \alpha$ and any neighborhood $s$ of $1$, the set $\{a\} \cdot s$ is a neighborhood of $a$.

IsOpen.mul_right theorem

(hs : IsOpen s) : IsOpen (s * t)

Full source

@[to_additive]
theorem IsOpen.mul_right (hs : IsOpen s) : IsOpen (s * t) := by
  rw [← image_op_smul]
  exact hs.smul_left

Openness of Right Multiplication by an Open Set in a Topological Group

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $s$ is open, then the product set $s \cdot t$ is open in $G$.

subset_interior_mul_left theorem

: interior s * t ⊆ interior (s * t)

Full source

@[to_additive]
theorem subset_interior_mul_left : interiorinterior s * t ⊆ interior (s * t) :=
  interior_maximal (Set.mul_subset_mul_right interior_subset) isOpen_interior.mul_right

Interior of Left Multiplication in Topological Groups

Informal description

For any subsets $s$ and $t$ of a topological group $G$, the product of the interior of $s$ with $t$ is contained in the interior of the product set $s \cdot t$, i.e., $\text{interior}(s) \cdot t \subseteq \text{interior}(s \cdot t)$.

subset_interior_mul' theorem

: interior s * interior t ⊆ interior (s * t)

Full source

@[to_additive]
theorem subset_interior_mul' : interiorinterior s * interior t ⊆ interior (s * t) :=
  (Set.mul_subset_mul_left interior_subset).trans subset_interior_mul_left

Interior of Product Set Contains Product of Interiors in Topological Groups

Informal description

For any subsets $s$ and $t$ of a topological group $G$, the product of their interiors is contained in the interior of their product set, i.e., $\text{interior}(s) \cdot \text{interior}(t) \subseteq \text{interior}(s \cdot t)$.

mul_singleton_mem_nhds theorem

(a : α) {b : α} (h : s ∈ 𝓝 b) : s * { a } ∈ 𝓝 (b * a)

Full source

@[to_additive]
theorem mul_singleton_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : s * {a} ∈ 𝓝 (b * a) := by
  rw [mul_singleton]
  exact smul_mem_nhds_smul (op a) h

Neighborhood preservation under right multiplication in topological groups

Informal description

Let $G$ be a topological group and let $s$ be a subset of $G$. For any elements $a, b \in G$, if $s$ is a neighborhood of $b$ in $G$, then the pointwise product $s \cdot \{a\}$ is a neighborhood of $b \cdot a$. Here: - $s \cdot \{a\}$ denotes the set $\{x \cdot a \mid x \in s\}$ - $\mathcal{N}(x)$ denotes the neighborhood filter at point $x$ in $G$

mul_singleton_mem_nhds_of_nhds_one theorem

(a : α) (h : s ∈ 𝓝 (1 : α)) : s * { a } ∈ 𝓝 a

Full source

@[to_additive]
theorem mul_singleton_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : s * {a} ∈ 𝓝 a := by
  simpa only [one_mul] using mul_singleton_mem_nhds a h

Neighborhood of identity multiplied by singleton yields neighborhood in topological groups

Informal description

Let $G$ be a topological group and let $s$ be a subset of $G$. For any element $a \in G$, if $s$ is a neighborhood of the identity element $1 \in G$, then the pointwise product $s \cdot \{a\}$ is a neighborhood of $a$. Here: - $s \cdot \{a\}$ denotes the set $\{x \cdot a \mid x \in s\}$ - $\mathcal{N}(x)$ denotes the neighborhood filter at point $x$ in $G$

IsOpen.div_left theorem

(ht : IsOpen t) : IsOpen (s / t)

Full source

@[to_additive]
theorem IsOpen.div_left (ht : IsOpen t) : IsOpen (s / t) := by
  rw [← iUnion_div_left_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

Openness of Left Quotient Set in Topological Groups

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $t$ is open in $G$, then the left quotient set $s / t := \{x \in G \mid \exists y \in s, \exists z \in t, x = y / z\}$ is open in $G$.

IsOpen.div_right theorem

(hs : IsOpen s) : IsOpen (s / t)

Full source

@[to_additive]
theorem IsOpen.div_right (hs : IsOpen s) : IsOpen (s / t) := by
  rw [← iUnion_div_right_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

Openness of Right Quotient Set in Topological Groups

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $s$ is open, then the right quotient set $s / t = \{x / y \mid x \in s, y \in t\}$ is also open.

subset_interior_div_left theorem

: interior s / t ⊆ interior (s / t)

Full source

@[to_additive]
theorem subset_interior_div_left : interiorinterior s / t ⊆ interior (s / t) :=
  interior_maximal (div_subset_div_right interior_subset) isOpen_interior.div_right

Inclusion of Right Quotient of Interior in Interior of Right Quotient

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. The right quotient of the interior of $s$ by $t$ is contained in the interior of the right quotient of $s$ by $t$, i.e., $$\text{interior}(s) / t \subseteq \text{interior}(s / t).$$

subset_interior_div theorem

: interior s / interior t ⊆ interior (s / t)

Full source

@[to_additive]
theorem subset_interior_div : interiorinterior s / interior t ⊆ interior (s / t) :=
  (div_subset_div_left interior_subset).trans subset_interior_div_left

Inclusion of Quotient of Interiors in Interior of Quotient in Topological Group

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. The right quotient of the interior of $s$ by the interior of $t$ is contained in the interior of the right quotient of $s$ by $t$, i.e., $$\text{interior}(s) / \text{interior}(t) \subseteq \text{interior}(s / t).$$

IsOpen.mul_closure theorem

(hs : IsOpen s) (t : Set G) : s * closure t = s * t

Full source

@[to_additive]
theorem IsOpen.mul_closure (hs : IsOpen s) (t : Set G) : s * closure t = s * t := by
  refine (mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)
  rw [mem_closure_iff] at hb
  have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, Set.inv_mem_inv.2 ha, a * b, rfl, inv_mul_cancel_left _ _⟩
  obtain ⟨_, ⟨c, hc, d, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU
  exact ⟨c⁻¹, hc, _, hcs, inv_mul_cancel_left _ _⟩

Open Set Multiplied by Closure Equals Open Set Multiplied by Set in Topological Group

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $s$ is open, then the product set $s \cdot \overline{t}$ is equal to $s \cdot t$, where $\overline{t}$ denotes the closure of $t$.

IsOpen.closure_mul theorem

(ht : IsOpen t) (s : Set G) : closure s * t = s * t

Full source

@[to_additive]
theorem IsOpen.closure_mul (ht : IsOpen t) (s : Set G) : closure s * t = s * t := by
  rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]

Closure of Set Multiplied by Open Set Equals Set Multiplied by Open Set in Topological Group

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $t$ is open, then the product set $\overline{s} \cdot t$ is equal to $s \cdot t$, where $\overline{s}$ denotes the closure of $s$.

IsOpen.div_closure theorem

(hs : IsOpen s) (t : Set G) : s / closure t = s / t

Full source

@[to_additive]
theorem IsOpen.div_closure (hs : IsOpen s) (t : Set G) : s / closure t = s / t := by
  simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]

Open Set Divided by Closure Equals Open Set Divided by Set in Topological Group

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $s$ is open, then the set of quotients $s / \overline{t}$ is equal to $s / t$, where $\overline{t}$ denotes the topological closure of $t$ and $/$ denotes pointwise division (i.e., $s / t = \{x / y \mid x \in s, y \in t\}$).

IsOpen.closure_div theorem

(ht : IsOpen t) (s : Set G) : closure s / t = s / t

Full source

@[to_additive]
theorem IsOpen.closure_div (ht : IsOpen t) (s : Set G) : closure s / t = s / t := by
  simp_rw [div_eq_mul_inv, ht.inv.closure_mul]

Open Set Property for Division with Closure in Topological Groups

Informal description

Let $G$ be a topological group and let $s, t \subseteq G$ be subsets. If $t$ is open, then the set of quotients $\overline{s} / t$ is equal to $s / t$, where $\overline{s}$ denotes the topological closure of $s$ and $/$ denotes pointwise division (i.e., $s / t = \{x / y \mid x \in s, y \in t\}$).

IsClosed.mul_left_of_isCompact theorem

(ht : IsClosed t) (hs : IsCompact s) : IsClosed (s * t)

Full source

@[to_additive]
theorem IsClosed.mul_left_of_isCompact (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s * t) :=
  ht.smul_left_of_isCompact hs

Closedness of compact-closed product in topological groups

Informal description

Let $G$ be a topological group with continuous multiplication, and let $s, t \subseteq G$ be subsets. If $s$ is compact and $t$ is closed, then their pointwise product $s \cdot t$ is closed in $G$.

IsClosed.mul_right_of_isCompact theorem

(ht : IsClosed t) (hs : IsCompact s) : IsClosed (t * s)

Full source

@[to_additive]
theorem IsClosed.mul_right_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
    IsClosed (t * s) := by
  rw [← image_op_smul]
  exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)

Closedness of Right Product with Compact Set in Topological Groups

Informal description

Let $G$ be a topological group with continuous multiplication, and let $s, t \subseteq G$ be subsets. If $s$ is compact and $t$ is closed, then their pointwise product $t \cdot s$ is closed in $G$.

subset_mul_closure_one theorem

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

Full source

@[to_additive]
lemma subset_mul_closure_one {G} [MulOneClass G] [TopologicalSpace G] (s : Set G) :
    s ⊆ s * (closure {1} : Set G) := by
  have : s ⊆ s * ({1} : Set G) := by simp
  exact this.trans (smul_subset_smul_left subset_closure)

Subset Inclusion in Product with Closure of Identity

Informal description

Let $G$ be a topological space equipped with a multiplicative monoid structure. For any subset $s \subseteq G$, we have $s \subseteq s \cdot \overline{\{1\}}$, where $\overline{\{1\}}$ denotes the topological closure of the singleton set containing the multiplicative identity $1 \in G$.

IsCompact.mul_closure_one_eq_closure theorem

{K : Set G} (hK : IsCompact K) : K * (closure { 1 } : Set G) = closure K

Full source

@[to_additive]
lemma IsCompact.mul_closure_one_eq_closure {K : Set G} (hK : IsCompact K) :
    K * (closure {1} : Set G) = closure K := by
  apply Subset.antisymm ?_ ?_
  · calc
    K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
      smul_subset_smul_right subset_closure
    _ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
    _ = closure K := by simp
  · have : IsClosed (K * (closure {1} : Set G)) :=
      IsClosed.smul_left_of_isCompact isClosed_closure hK
    rw [IsClosed.closure_subset_iff this]
    exact subset_mul_closure_one K

Compact Sets in Topological Groups Satisfy $K \cdot \overline{\{1\}} = \overline{K}$

Informal description

Let $G$ be a topological group and $K \subseteq G$ a compact subset. Then the product of $K$ with the closure of the singleton set $\{1\}$ (where $1$ is the group identity) equals the closure of $K$, i.e., $K \cdot \overline{\{1\}} = \overline{K}$.

IsClosed.mul_closure_one_eq theorem

{F : Set G} (hF : IsClosed F) : F * (closure { 1 } : Set G) = F

Full source

@[to_additive]
lemma IsClosed.mul_closure_one_eq {F : Set G} (hF : IsClosed F) :
    F * (closure {1} : Set G) = F := by
  refine Subset.antisymm ?_ (subset_mul_closure_one F)
  calc
  F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
  _ = F := by simp [hF.closure_eq]

Closed Sets are Invariant under Multiplication with Closure of Identity in Topological Groups

Informal description

Let $G$ be a topological group and $F \subseteq G$ a closed subset. Then the product of $F$ with the closure of the singleton set $\{1\}$ (where $1$ is the group identity) equals $F$ itself, i.e., $F \cdot \overline{\{1\}} = F$.

compl_mul_closure_one_eq theorem

{t : Set G} (ht : t * (closure { 1 } : Set G) = t) : tᶜ * (closure { 1 } : Set G) = tᶜ

Full source

@[to_additive]
lemma compl_mul_closure_one_eq {t : Set G} (ht : t * (closure {1} : Set G) = t) :
    tᶜ * (closure {1} : Set G) = tᶜ := by
  refine Subset.antisymm ?_ (subset_mul_closure_one tᶜ)
  rintro - ⟨x, hx, g, hg, rfl⟩
  by_contra H
  have : x ∈ t * (closure {1} : Set G) := by
    rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
    simp only [smul_eq_mul, mem_compl_iff, not_not] at H
    exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩
  rw [ht] at this
  exact hx this

Complement Stability under Right Multiplication by Identity Closure in Topological Groups

Informal description

Let $G$ be a topological group and $t \subseteq G$ a subset satisfying $t \cdot \overline{\{1\}} = t$, where $\overline{\{1\}}$ denotes the topological closure of the singleton set containing the identity element. Then the complement $t^c$ satisfies $t^c \cdot \overline{\{1\}} = t^c$.

compl_mul_closure_one_eq_iff theorem

{t : Set G} : tᶜ * (closure { 1 } : Set G) = tᶜ ↔ t * (closure { 1 } : Set G) = t

Full source

@[to_additive]
lemma compl_mul_closure_one_eq_iff {t : Set G} :
    tᶜtᶜ * (closure {1} : Set G) = tᶜ ↔ t * (closure {1} : Set G) = t :=
  ⟨fun h ↦ by simpa using compl_mul_closure_one_eq h, fun h ↦ compl_mul_closure_one_eq h⟩

Complement Stability under Right Multiplication by Identity Closure in Topological Groups: $t^c \cdot \overline{\{1\}} = t^c \leftrightarrow t \cdot \overline{\{1\}} = t$

Informal description

For any subset $t$ of a topological group $G$, the complement $t^c$ satisfies $t^c \cdot \overline{\{1\}} = t^c$ if and only if $t \cdot \overline{\{1\}} = t$, where $\overline{\{1\}}$ denotes the topological closure of the singleton set containing the identity element.

IsOpen.mul_closure_one_eq theorem

{U : Set G} (hU : IsOpen U) : U * (closure { 1 } : Set G) = U

Full source

@[to_additive]
lemma IsOpen.mul_closure_one_eq {U : Set G} (hU : IsOpen U) :
    U * (closure {1} : Set G) = U :=
  compl_mul_closure_one_eq_iff.1 (hU.isClosed_compl.mul_closure_one_eq)

Open Sets are Invariant under Multiplication with Closure of Identity in Topological Groups

Informal description

Let $G$ be a topological group and $U \subseteq G$ an open subset. Then the product of $U$ with the closure of the singleton set $\{1\}$ (where $1$ is the group identity) equals $U$ itself, i.e., $U \cdot \overline{\{1\}} = U$.

IsTopologicalGroup.regularSpace instance

: RegularSpace G

Full source

@[to_additive]
instance (priority := 100) IsTopologicalGroup.regularSpace : RegularSpace G := by
  refine .of_exists_mem_nhds_isClosed_subset fun a s hs ↦ ?_
  have : Tendsto (fun p : G × G => p.1 * p.2) (𝓝 (a, 1)) (𝓝 a) :=
    continuous_mul.tendsto' _ _ (mul_one a)
  rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩
  rw [← image_subset_iff, image_prod] at hUV
  refine ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, ?_⟩
  calc
    closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
    _ = U * interior V := isOpen_interior.closure_mul U
    _ ⊆ U * Vcalc
    closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
    _ = U * interior V := isOpen_interior.closure_mul U
    _ ⊆ U * V := mul_subset_mul_left interior_subset
    _ ⊆ s := hUV

Topological Groups are Regular Spaces

Informal description

Every topological group is a regular space.

group_inseparable_iff theorem

{x y : G} : Inseparable x y ↔ x / y ∈ closure (1 : Set G)

Full source

@[to_additive]
theorem group_inseparable_iff {x y : G} : InseparableInseparable x y ↔ x / y ∈ closure (1 : Set G) := by
  rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable,
    ← (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff]
  simp [div_eq_mul_inv]

Inseparability Criterion in Topological Groups: $x \sim y \leftrightarrow x/y \in \overline{\{1\}}$

Informal description

For any two elements $x$ and $y$ in a topological group $G$, the points $x$ and $y$ are topologically inseparable if and only if the quotient $x / y$ belongs to the closure of the singleton set $\{1\}$, where $1$ is the identity element of $G$.

IsTopologicalGroup.t2Space_iff_one_closed theorem

: T2Space G ↔ IsClosed ({ 1 } : Set G)

Full source

@[to_additive]
theorem IsTopologicalGroup.t2Space_iff_one_closed : T2SpaceT2Space G ↔ IsClosed ({1} : Set G) :=
  ⟨fun _ ↦ isClosed_singleton, fun h ↦
    have := IsTopologicalGroup.t1Space G h; inferInstance⟩

Hausdorff Criterion for Topological Groups: $\{1\}$ Closed $\iff$ $T_2$

Informal description

A topological group $G$ is a Hausdorff space if and only if the singleton set $\{1\}$ is closed in $G$.

IsTopologicalGroup.t2Space_of_one_sep theorem

(H : ∀ x : G, x ≠ 1 → ∃ U ∈ 𝓝 (1 : G), x ∉ U) : T2Space G

Full source

@[to_additive]
theorem IsTopologicalGroup.t2Space_of_one_sep (H : ∀ x : G, x ≠ 1 → ∃ U ∈ 𝓝 (1 : G), x ∉ U) :
    T2Space G := by
  suffices T1Space G from inferInstance
  refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_
  rcases H (x * y⁻¹) (by rwa [Ne, mul_inv_eq_one]) with ⟨U, hU₁, hU⟩
  exact hU <| mem_of_mem_nhds <| hspec.map (continuous_mul_right y⁻¹) (by rwa [mul_inv_cancel])

Hausdorff Criterion for Topological Groups via Neighborhood Separation of Identity

Informal description

Let $G$ be a topological group. If for every $x \in G$ with $x \neq 1$, there exists a neighborhood $U$ of $1$ such that $x \notin U$, then $G$ is a Hausdorff space.

exists_closed_nhds_one_inv_eq_mul_subset theorem

{U : Set G} (hU : U ∈ 𝓝 1) : ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Full source

/-- 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`. -/
@[to_additive "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_one_inv_eq_mul_subset {U : Set G} (hU : U ∈ 𝓝 1) :
    ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U := by
  rcases exists_open_nhds_one_mul_subset hU with ⟨V, V_open, V_mem, hV⟩
  rcases exists_mem_nhds_isClosed_subset (V_open.mem_nhds V_mem) with ⟨W, W_mem, W_closed, hW⟩
  refine ⟨W ∩ W⁻¹, Filter.inter_mem W_mem (inv_mem_nhds_one G W_mem), W_closed.inter W_closed.inv,
    by simp [inter_comm], ?_⟩
  calc
  W ∩ W⁻¹ * (W ∩ W⁻¹)
    ⊆ W * W := mul_subset_mul inter_subset_left inter_subset_left
  _ ⊆ V * Vcalc
  W ∩ W⁻¹ * (W ∩ W⁻¹)
    ⊆ W * W := mul_subset_mul inter_subset_left inter_subset_left
  _ ⊆ V * V := mul_subset_mul hW hW
  _ ⊆ U := hV

Existence of Symmetric Closed Neighborhood with Square Contained in Given Neighborhood

Informal description

For any neighborhood $U$ of the identity element $1$ in a topological group $G$, there exists a closed neighborhood $V$ of $1$ such that $V$ is symmetric (i.e., $V^{-1} = V$) and the product set $V \cdot V$ is contained in $U$.

IsCompact.locallyCompactSpace_of_mem_nhds_of_group theorem

{K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ 𝓝 x) : LocallyCompactSpace G

Full source

/-- If a point in a topological group has a compact neighborhood, then the group is
locally compact. -/
@[to_additive]
theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {K : Set G} (hK : IsCompact K) {x : G}
    (h : K ∈ 𝓝 x) : LocallyCompactSpace G := by
  suffices WeaklyLocallyCompactSpace G from inferInstance
  refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩
  · exact hK.smul _
  · rw [← preimage_smul_inv]
    exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)

Local compactness of topological groups via compact neighborhoods

Informal description

Let $G$ be a topological group and $K \subseteq G$ a compact subset. If $K$ is a neighborhood of some point $x \in G$, then $G$ is locally compact.