# Topological group with zero #

In this file we define HasContinuousInv₀ to be a mixin typeclass a type with Inv and Zero (e.g., a GroupWithZero) such that fun x ↦ x⁻¹ is continuous at all nonzero points. Any normed (semi)field has this property. Currently the only example of HasContinuousInv₀ in mathlib which is not a normed field is the type NNReal (a.k.a. ℝ≥0) of nonnegative real numbers.

Then we prove lemmas about continuity of x ↦ x⁻¹ and f / g providing dot-style *.inv₀ and *.div operations on Filter.Tendsto, ContinuousAt, ContinuousWithinAt, ContinuousOn, and Continuous. As a special case, we provide *.div_const operations that require only DivInvMonoid and ContinuousMul instances.

All lemmas about (⁻¹) use inv₀ in their names because lemmas without ₀ are used for TopologicalGroups. We also use ' in the typeclass name HasContinuousInv₀ for the sake of consistency of notation.

On a GroupWithZero with continuous multiplication, we also define left and right multiplication as homeomorphisms.

### A DivInvMonoid with continuous multiplication #

If G₀ is a DivInvMonoid with continuous (*), then (/y) is continuous for any y. In this section we prove lemmas that immediately follow from this fact providing *.div_const dot-style operations on Filter.Tendsto, ContinuousAt, ContinuousWithinAt, ContinuousOn, and Continuous.

theorem Filter.Tendsto.div_const {α : Type u_1} {G₀ : Type u_3} [] [] [] {f : αG₀} {l : } {x : G₀} (hf : Filter.Tendsto f l (nhds x)) (y : G₀) :
Filter.Tendsto (fun (a : α) => f a / y) l (nhds (x / y))
theorem ContinuousAt.div_const {α : Type u_1} {G₀ : Type u_3} [] [] [] {f : αG₀} [] {a : α} (hf : ) (y : G₀) :
ContinuousAt (fun (x : α) => f x / y) a
theorem ContinuousWithinAt.div_const {α : Type u_1} {G₀ : Type u_3} [] [] [] {f : αG₀} {s : Set α} [] {a : α} (hf : ) (y : G₀) :
ContinuousWithinAt (fun (x : α) => f x / y) s a
theorem ContinuousOn.div_const {α : Type u_1} {G₀ : Type u_3} [] [] [] {f : αG₀} {s : Set α} [] (hf : ) (y : G₀) :
ContinuousOn (fun (x : α) => f x / y) s
theorem Continuous.div_const {α : Type u_1} {G₀ : Type u_3} [] [] [] {f : αG₀} [] (hf : ) (y : G₀) :
Continuous fun (x : α) => f x / y
class HasContinuousInv₀ (G₀ : Type u_4) [Zero G₀] [Inv G₀] [] :

A type with 0 and Inv such that fun x ↦ x⁻¹ is continuous at all nonzero points. Any normed (semi)field has this property.

• continuousAt_inv₀ : ∀ ⦃x : G₀⦄, x 0ContinuousAt Inv.inv x

The map fun x ↦ x⁻¹ is continuous at all nonzero points.

Instances
theorem HasContinuousInv₀.continuousAt_inv₀ {G₀ : Type u_4} [Zero G₀] [Inv G₀] [] [self : ] ⦃x : G₀ :
x 0ContinuousAt Inv.inv x

The map fun x ↦ x⁻¹ is continuous at all nonzero points.

### Continuity of fun x ↦ x⁻¹ at a non-zero point #

We define HasContinuousInv₀ to be a GroupWithZero such that the operation x ↦ x⁻¹ is continuous at all nonzero points. In this section we prove dot-style *.inv₀ lemmas for Filter.Tendsto, ContinuousAt, ContinuousWithinAt, ContinuousOn, and Continuous.

theorem tendsto_inv₀ {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] {x : G₀} (hx : x 0) :
Filter.Tendsto Inv.inv (nhds x) ()
theorem continuousOn_inv₀ {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] :
ContinuousOn Inv.inv {0}
theorem Filter.Tendsto.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] {l : } {f : αG₀} {a : G₀} (hf : Filter.Tendsto f l (nhds a)) (ha : a 0) :
Filter.Tendsto (fun (x : α) => (f x)⁻¹) l ()

If a function converges to a nonzero value, its inverse converges to the inverse of this value. We use the name Filter.Tendsto.inv₀ as Filter.Tendsto.inv is already used in multiplicative topological groups.

theorem ContinuousWithinAt.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] {f : αG₀} {s : Set α} {a : α} [] (hf : ) (ha : f a 0) :
ContinuousWithinAt (fun (x : α) => (f x)⁻¹) s a
theorem ContinuousAt.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] {f : αG₀} {a : α} [] (hf : ) (ha : f a 0) :
ContinuousAt (fun (x : α) => (f x)⁻¹) a
theorem Continuous.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] {f : αG₀} [] (hf : ) (h0 : ∀ (x : α), f x 0) :
Continuous fun (x : α) => (f x)⁻¹
theorem ContinuousOn.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [] [] {f : αG₀} {s : Set α} [] (hf : ) (h0 : xs, f x 0) :
ContinuousOn (fun (x : α) => (f x)⁻¹) s
theorem Units.embedding_val₀ {G₀ : Type u_3} [] [] [] :
Embedding Units.val

If G₀ is a group with zero with topology such that x ↦ x⁻¹ is continuous at all nonzero points. Then the coercion G₀ˣ → G₀ is a topological embedding.

theorem nhds_inv₀ {G₀ : Type u_3} [] [] [] {x : G₀} (hx : x 0) :
theorem tendsto_inv_iff₀ {α : Type u_1} {G₀ : Type u_3} [] [] [] {x : G₀} {l : } {f : αG₀} (hx : x 0) :
Filter.Tendsto (fun (x : α) => (f x)⁻¹) l () Filter.Tendsto f l (nhds x)

### Continuity of division #

If G₀ is a GroupWithZero with x ↦ x⁻¹ continuous at all nonzero points and (*), then division (/) is continuous at any point where the denominator is continuous.

theorem Filter.Tendsto.div {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} {l : } {a : G₀} {b : G₀} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) (hy : b 0) :
Filter.Tendsto (f / g) l (nhds (a / b))
theorem Filter.tendsto_mul_iff_of_ne_zero {α : Type u_1} {G₀ : Type u_3} [] [] [] [] [T1Space G₀] {f : αG₀} {g : αG₀} {l : } {x : G₀} {y : G₀} (hg : Filter.Tendsto g l (nhds y)) (hy : y 0) :
Filter.Tendsto (fun (n : α) => f n * g n) l (nhds (x * y)) Filter.Tendsto f l (nhds x)
theorem ContinuousWithinAt.div {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] {s : Set α} {a : α} (hf : ) (hg : ) (h₀ : g a 0) :
theorem ContinuousOn.div {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] {s : Set α} (hf : ) (hg : ) (h₀ : xs, g x 0) :
ContinuousOn (f / g) s
theorem ContinuousAt.div {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] {a : α} (hf : ) (hg : ) (h₀ : g a 0) :
ContinuousAt (f / g) a

Continuity at a point of the result of dividing two functions continuous at that point, where the denominator is nonzero.

theorem Continuous.div {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] (hf : ) (hg : ) (h₀ : ∀ (x : α), g x 0) :
theorem continuousOn_div {G₀ : Type u_3} [] [] [] [] :
ContinuousOn (fun (p : G₀ × G₀) => p.1 / p.2) {p : G₀ × G₀ | p.2 0}
theorem Continuous.div₀ {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] (hf : ) (hg : ) (h₀ : ∀ (x : α), g x 0) :
Continuous fun (x : α) => f x / g x
theorem ContinuousAt.div₀ {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] {a : α} (hf : ) (hg : ) (h₀ : g a 0) :
ContinuousAt (fun (x : α) => f x / g x) a
theorem ContinuousOn.div₀ {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {g : αG₀} [] {s : Set α} (hf : ) (hg : ) (h₀ : xs, g x 0) :
ContinuousOn (fun (x : α) => f x / g x) s
theorem ContinuousAt.comp_div_cases {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [] [] [] [] [] [] {a : α} {f : αG₀} {g : αG₀} (h : αG₀β) (hf : ) (hg : ) (hh : g a 0ContinuousAt (h) (a, f a / g a)) (h2h : g a = 0Filter.Tendsto (h) (nhds a ×ˢ ) (nhds (h a 0))) :
ContinuousAt (fun (x : α) => h x (f x / g x)) a

The function f x / g x is discontinuous when g x = 0. However, under appropriate conditions, h x (f x / g x) is still continuous. The condition is that if g a = 0 then h x y must tend to h a 0 when x tends to a, with no information about y. This is represented by the ⊤ filter. Note: tendsto_prod_top_iff characterizes this convergence in uniform spaces. See also Filter.prod_top and Filter.mem_prod_top.

theorem Continuous.comp_div_cases {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [] [] [] [] [] [] {f : αG₀} {g : αG₀} (h : αG₀β) (hf : ) (hg : ) (hh : ∀ (a : α), g a 0ContinuousAt (h) (a, f a / g a)) (h2h : ∀ (a : α), g a = 0Filter.Tendsto (h) (nhds a ×ˢ ) (nhds (h a 0))) :
Continuous fun (x : α) => h x (f x / g x)

h x (f x / g x) is continuous under certain conditions, even if the denominator is sometimes 0. See docstring of ContinuousAt.comp_div_cases.

### Left and right multiplication as homeomorphisms #

def Homeomorph.mulLeft₀ {α : Type u_1} [] [] [] (c : α) (hc : c 0) :
α ≃ₜ α

Left multiplication by a nonzero element in a GroupWithZero with continuous multiplication is a homeomorphism of the underlying type.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
def Homeomorph.mulRight₀ {α : Type u_1} [] [] [] (c : α) (hc : c 0) :
α ≃ₜ α

Right multiplication by a nonzero element in a GroupWithZero with continuous multiplication is a homeomorphism of the underlying type.

Equations
• = let __src := ; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem Homeomorph.coe_mulLeft₀ {α : Type u_1} [] [] [] (c : α) (hc : c 0) :
() = fun (x : α) => c * x
@[simp]
theorem Homeomorph.mulLeft₀_symm_apply {α : Type u_1} [] [] [] (c : α) (hc : c 0) :
().symm = fun (x : α) => c⁻¹ * x
@[simp]
theorem Homeomorph.coe_mulRight₀ {α : Type u_1} [] [] [] (c : α) (hc : c 0) :
() = fun (x : α) => x * c
@[simp]
theorem Homeomorph.mulRight₀_symm_apply {α : Type u_1} [] [] [] (c : α) (hc : c 0) :
().symm = fun (x : α) => x * c⁻¹
theorem map_mul_left_nhds₀ {G₀ : Type u_3} [] [] [] {a : G₀} (ha : a 0) (b : G₀) :
Filter.map (fun (x : G₀) => a * x) (nhds b) = nhds (a * b)
theorem map_mul_left_nhds_one₀ {G₀ : Type u_3} [] [] [] {a : G₀} (ha : a 0) :
Filter.map (fun (x : G₀) => a * x) (nhds 1) = nhds a
theorem map_mul_right_nhds₀ {G₀ : Type u_3} [] [] [] {a : G₀} (ha : a 0) (b : G₀) :
Filter.map (fun (x : G₀) => x * a) (nhds b) = nhds (b * a)
theorem map_mul_right_nhds_one₀ {G₀ : Type u_3} [] [] [] {a : G₀} (ha : a 0) :
Filter.map (fun (x : G₀) => x * a) (nhds 1) = nhds a
theorem nhds_translation_mul_inv₀ {G₀ : Type u_3} [] [] [] {a : G₀} (ha : a 0) :
Filter.comap (fun (x : G₀) => x * a⁻¹) (nhds 1) = nhds a
theorem HasContinuousInv₀.of_nhds_one {G₀ : Type u_3} [] [] [] (h : Filter.Tendsto Inv.inv (nhds 1) (nhds 1)) :

If a group with zero has continuous multiplication and fun x ↦ x⁻¹ is continuous at one, then it is continuous at any unit.

theorem continuousAt_zpow₀ {G₀ : Type u_3} [] [] [] [] (x : G₀) (m : ) (h : x 0 0 m) :
ContinuousAt (fun (x : G₀) => x ^ m) x
theorem continuousOn_zpow₀ {G₀ : Type u_3} [] [] [] [] (m : ) :
ContinuousOn (fun (x : G₀) => x ^ m) {0}
theorem Filter.Tendsto.zpow₀ {α : Type u_1} {G₀ : Type u_3} [] [] [] [] {f : αG₀} {l : } {a : G₀} (hf : Filter.Tendsto f l (nhds a)) (m : ) (h : a 0 0 m) :
Filter.Tendsto (fun (x : α) => f x ^ m) l (nhds (a ^ m))
theorem ContinuousAt.zpow₀ {G₀ : Type u_3} [] [] [] [] {X : Type u_4} [] {a : X} {f : XG₀} (hf : ) (m : ) (h : f a 0 0 m) :
ContinuousAt (fun (x : X) => f x ^ m) a
theorem ContinuousWithinAt.zpow₀ {G₀ : Type u_3} [] [] [] [] {X : Type u_4} [] {a : X} {s : Set X} {f : XG₀} (hf : ) (m : ) (h : f a 0 0 m) :
ContinuousWithinAt (fun (x : X) => f x ^ m) s a
theorem ContinuousOn.zpow₀ {G₀ : Type u_3} [] [] [] [] {X : Type u_4} [] {s : Set X} {f : XG₀} (hf : ) (m : ) (h : as, f a 0 0 m) :
ContinuousOn (fun (x : X) => f x ^ m) s
theorem Continuous.zpow₀ {G₀ : Type u_3} [] [] [] [] {X : Type u_4} [] {f : XG₀} (hf : ) (m : ) (h0 : ∀ (a : X), f a 0 0 m) :
Continuous fun (x : X) => f x ^ m