Continuous division in topological groups

Continuity, homeomorphism, and neighborhood results for division and subtraction.

theorem Filter.Tendsto.div_const' {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Div G] [ContinuousDiv G] {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) (b : G) : Tendsto (fun (x : α) => f x / b) l (nhds (c / b))

theorem Filter.Tendsto.sub_const {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Sub G] [ContinuousSub G] {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) (b : G) : Tendsto (fun (x : α) => f x - b) l (nhds (c - b))

theorem Filter.tendsto_div_const_iff {α : Type u_2} {G : Type u_3} [GroupWithZero G] [TopologicalSpace G] [ContinuousDiv G] {b : G} (hb : b ≠ 0) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (x : α) => f x / b) l (nhds (c / b)) ↔ Tendsto f l (nhds c)

theorem Filter.tendsto_div_const_iff' {α : Type u_2} {G : Type u_3} [TopologicalSpace G] [Group G] [ContinuousDiv 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_sub_const_iff {α : Type u_2} {G : Type u_3} [TopologicalSpace G] [AddGroup G] [ContinuousSub 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_div' {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Div G] [ContinuousDiv G] (b : G) {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) : Tendsto (fun (x : α) => b / f x) l (nhds (b / c))

theorem Filter.Tendsto.const_sub {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Sub G] [ContinuousSub G] (b : G) {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (nhds c)) : Tendsto (fun (x : α) => b - f x) l (nhds (b - c))

theorem continuous_div_left' {G : Type u_1} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) : Continuous fun (x : G) => a / x

theorem continuous_sub_left {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) : Continuous fun (x : G) => a - x

theorem continuous_div_right' {G : Type u_1} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) : Continuous fun (x : G) => x / a

theorem continuous_sub_right {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) : Continuous fun (x : G) => x - a

theorem Filter.tendsto_const_div_iff' {G : Type u_1} {α : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (k : α) => b / f k) l (nhds (b / c)) ↔ Tendsto f l (nhds c)

theorem Filter.tendsto_const_sub_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (k : α) => b - f k) l (nhds (b - c)) ↔ Tendsto f l (nhds c)

@[deprecated Filter.tendsto_const_div_iff' (since := "2026-02-03")]

theorem Filter.tendsto_const_div_iff {G : Type u_1} {α : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (b : G) {c : G} {f : α → G} {l : Filter α} : Tendsto (fun (k : α) => b / f k) l (nhds (b / c)) ↔ Tendsto f l (nhds c)

Alias of Filter.tendsto_const_div_iff'.

def Homeomorph.divLeft {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : G ≃ₜ G

A version of Homeomorph.mulLeft a b⁻¹ that is defeq to a / b.

Equations

• Homeomorph.divLeft x = { toEquiv := Equiv.divLeft x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.subLeft {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x : G) : G ≃ₜ G

A version of Homeomorph.addLeft a (-b) that is defeq to a - b.

Equations

• Homeomorph.subLeft x = { toEquiv := Equiv.subLeft x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.divLeft_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x b : G) : (divLeft x).symm b = b⁻¹ * x

@[simp]

theorem Homeomorph.subLeft_symm_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (subLeft x).symm b = -b + x

@[simp]

theorem Homeomorph.divLeft_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x b : G) : (divLeft x) b = x / b

@[simp]

theorem Homeomorph.subLeft_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (subLeft x) b = x - b

@[simp]

theorem Homeomorph.coe_divLeft {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : G) : ⇑(divLeft a) = fun (x : G) => a / x

@[simp]

theorem Homeomorph.coe_subLeft {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : ⇑(subLeft a) = fun (x : G) => a - x

theorem isOpenMap_div_left {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : G) : IsOpenMap fun (x : G) => a / x

theorem isOpenMap_sub_left {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsOpenMap fun (x : G) => a - x

theorem isClosedMap_div_left {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : G) : IsClosedMap fun (x : G) => a / x

theorem isClosedMap_sub_left {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsClosedMap fun (x : G) => a - x

def Homeomorph.divRight {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : G ≃ₜ G

A version of Homeomorph.mulRight a⁻¹ b that is defeq to b / a.

Equations

• Homeomorph.divRight x = { toEquiv := Equiv.divRight x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.subRight {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x : G) : G ≃ₜ G

A version of Homeomorph.addRight (-a) b that is defeq to b - a.

Equations

• Homeomorph.subRight x = { toEquiv := Equiv.subRight x, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.divRight_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x b : G) : (divRight x) b = b / x

@[simp]

theorem Homeomorph.divRight_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x b : G) : (divRight x).symm b = b * x

@[simp]

theorem Homeomorph.subRight_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (subRight x) b = b - x

@[simp]

theorem Homeomorph.subRight_symm_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (subRight x).symm b = b + x

@[simp]

theorem Homeomorph.coe_divRight {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : G) : ⇑(divRight a) = fun (x : G) => x / a

@[simp]

theorem Homeomorph.coe_subRight {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : ⇑(subRight a) = fun (x : G) => x - a

theorem isOpenMap_div_right {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : G) : IsOpenMap fun (x : G) => x / a

theorem isOpenMap_sub_right {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsOpenMap fun (x : G) => x - a

theorem isClosedMap_div_right {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : G) : IsClosedMap fun (x : G) => x / a

theorem isClosedMap_sub_right {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsClosedMap fun (x : G) => x - a

theorem tendsto_div_nhds_one_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {α : Type u_3} {l : Filter α} {x : G} {u : α → G} : Filter.Tendsto (fun (x_1 : α) => u x_1 / x) l (nhds 1) ↔ Filter.Tendsto u l (nhds x)

theorem tendsto_sub_nhds_zero_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} {x : G} {u : α → G} : Filter.Tendsto (fun (x_1 : α) => u x_1 - x) l (nhds 0) ↔ Filter.Tendsto u l (nhds x)

theorem tendsto_div_nhds_one_iff_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {α : Type u_3} {l : Filter α} [l.NeBot] [T2Space G] {f g : α → G} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 1) ↔ a = b

If f → a and g → b along a nontrivial filter on the domain, valued in a Hausdorff topological group, then f / g → 1 if and only if a = b.

theorem tendsto_sub_nhds_zero_iff_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} [l.NeBot] [T2Space G] {f g : α → G} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun (x : α) => f x - g x) l (nhds 0) ↔ a = b

theorem eq_of_tendsto_div_nhds_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {α : Type u_3} {l : Filter α} [l.NeBot] [T2Space G] {f g : α → G} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 1) → a = b

Alias of the forward direction of tendsto_div_nhds_one_iff_eq.

---

If f → a and g → b along a nontrivial filter on the domain, valued in a Hausdorff topological group, then f / g → 1 if and only if a = b.

theorem eq_of_tendsto_sub_nhds_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} [l.NeBot] [T2Space G] {f g : α → G} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun (x : α) => f x - g x) l (nhds 0) → a = b

Alias of the forward direction of tendsto_sub_nhds_zero_iff_eq.

theorem nhds_translation_div {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 / x) (nhds 1) = nhds x

theorem nhds_translation_sub {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x : G) : Filter.comap (fun (x_1 : G) => x_1 - x) (nhds 0) = nhds x

@[simp]

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

@[simp]

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

@[simp]

theorem Filter.map_divRight_nhds {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {c a : G} : map (fun (x : G) => x / c) (nhds a) = nhds (a / c)

@[simp]

theorem Filter.map_subRight_nhds {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G} : map (fun (x : G) => x - c) (nhds a) = nhds (a - c)

@[simp]

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

@[simp]

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

@[simp]

theorem Filter.map_divLeft_nhds {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {c a : G} : map (fun (x : G) => c / x) (nhds a) = nhds (c / a)

@[simp]

theorem Filter.map_subLeft_nhds {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G} : map (fun (x : G) => c - x) (nhds a) = nhds (c - a)