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} [DivInvMonoid G₀] [TopologicalSpace G₀] [ContinuousMul G₀] {f : α → G₀} {l : Filter α} {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} [DivInvMonoid G₀] [TopologicalSpace G₀] [ContinuousMul G₀] {f : α → G₀} [TopologicalSpace α] {a : α} (hf : ContinuousAt f a) (y : G₀) : ContinuousAt (fun (x : α) => f x / y) a

theorem ContinuousWithinAt.div_const {α : Type u_1} {G₀ : Type u_3} [DivInvMonoid G₀] [TopologicalSpace G₀] [ContinuousMul G₀] {f : α → G₀} {s : Set α} [TopologicalSpace α] {a : α} (hf : ContinuousWithinAt f s a) (y : G₀) : ContinuousWithinAt (fun (x : α) => f x / y) s a

theorem ContinuousOn.div_const {α : Type u_1} {G₀ : Type u_3} [DivInvMonoid G₀] [TopologicalSpace G₀] [ContinuousMul G₀] {f : α → G₀} {s : Set α} [TopologicalSpace α] (hf : ContinuousOn f s) (y : G₀) : ContinuousOn (fun (x : α) => f x / y) s

theorem Continuous.div_const {α : Type u_1} {G₀ : Type u_3} [DivInvMonoid G₀] [TopologicalSpace G₀] [ContinuousMul G₀] {f : α → G₀} [TopologicalSpace α] (hf : Continuous f) (y : G₀) : Continuous fun (x : α) => f x / y

class HasContinuousInv₀ (G₀ : Type u_4) [Zero G₀] [Inv G₀] [TopologicalSpace G₀] : Prop

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 ≠ 0 → ContinuousAt 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₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {x : G₀} (hx : x ≠ 0) : Filter.Tendsto Inv.inv (nhds x) (nhds x⁻¹)

theorem continuousOn_inv₀ {G₀ : Type u_3} [Zero G₀] [Inv G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] : ContinuousOn Inv.inv {0}ᶜ

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

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₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {f : α → G₀} {s : Set α} {a : α} [TopologicalSpace α] (hf : ContinuousWithinAt f s a) (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₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {f : α → G₀} {a : α} [TopologicalSpace α] (hf : ContinuousAt f a) (ha : f a ≠ 0) : ContinuousAt (fun (x : α) => (f x)⁻¹) a

theorem Continuous.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {f : α → G₀} [TopologicalSpace α] (hf : Continuous f) (h0 : ∀ (x : α), f x ≠ 0) : Continuous fun (x : α) => (f x)⁻¹

theorem ContinuousOn.inv₀ {α : Type u_1} {G₀ : Type u_3} [Zero G₀] [Inv G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {f : α → G₀} {s : Set α} [TopologicalSpace α] (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContinuousOn (fun (x : α) => (f x)⁻¹) s

theorem Units.embedding_val₀ {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] : 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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {x : G₀} (hx : x ≠ 0) : nhds x⁻¹ = (nhds x)⁻¹

theorem tendsto_inv_iff₀ {α : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {x : G₀} {l : Filter α} {f : α → G₀} (hx : x ≠ 0) : Filter.Tendsto (fun (x : α) => (f x)⁻¹) l (nhds x⁻¹) ↔ 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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} {l : Filter α} {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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] [T1Space G₀] {f : α → G₀} {g : α → G₀} {l : Filter α} {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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) (h₀ : g a ≠ 0) : ContinuousWithinAt (f / g) s a

theorem ContinuousOn.div {α : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContinuousOn (f / g) s

theorem ContinuousAt.div {α : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] {a : α} (hf : ContinuousAt f a) (hg : ContinuousAt g a) (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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ (x : α), g x ≠ 0) : Continuous (f / g)

theorem continuousOn_div {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] : 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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ (x : α), g x ≠ 0) : Continuous fun (x : α) => f x / g x

theorem ContinuousAt.div₀ {α : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] {a : α} (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) : ContinuousAt (fun (x : α) => f x / g x) a

theorem ContinuousOn.div₀ {α : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {g : α → G₀} [TopologicalSpace α] {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, 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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] [TopologicalSpace α] [TopologicalSpace β] {a : α} {f : α → G₀} {g : α → G₀} (h : α → G₀ → β) (hf : ContinuousAt f a) (hg : ContinuousAt g a) (hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)) (h2h : g a = 0 → Filter.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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] [TopologicalSpace α] [TopologicalSpace β] {f : α → G₀} {g : α → G₀} (h : α → G₀ → β) (hf : Continuous f) (hg : Continuous g) (hh : ∀ (a : α), g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)) (h2h : ∀ (a : α), g a = 0 → Filter.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} [TopologicalSpace α] [GroupWithZero α] [ContinuousMul α] (c : α) (hc : c ≠ 0) : α ≃ₜ α

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

Equations

• Homeomorph.mulLeft₀ c hc = let __src := Equiv.mulLeft₀ c hc; { toEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.mulRight₀ {α : Type u_1} [TopologicalSpace α] [GroupWithZero α] [ContinuousMul α] (c : α) (hc : c ≠ 0) : α ≃ₜ α

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

Equations

• Homeomorph.mulRight₀ c hc = let __src := Equiv.mulRight₀ c hc; { toEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.coe_mulLeft₀ {α : Type u_1} [TopologicalSpace α] [GroupWithZero α] [ContinuousMul α] (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulLeft₀ c hc) = fun (x : α) => c * x

@[simp]

theorem Homeomorph.mulLeft₀_symm_apply {α : Type u_1} [TopologicalSpace α] [GroupWithZero α] [ContinuousMul α] (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.symm (Homeomorph.mulLeft₀ c hc)) = fun (x : α) => c⁻¹ * x

@[simp]

theorem Homeomorph.coe_mulRight₀ {α : Type u_1} [TopologicalSpace α] [GroupWithZero α] [ContinuousMul α] (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulRight₀ c hc) = fun (x : α) => x * c

@[simp]

theorem Homeomorph.mulRight₀_symm_apply {α : Type u_1} [TopologicalSpace α] [GroupWithZero α] [ContinuousMul α] (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.symm (Homeomorph.mulRight₀ c hc)) = fun (x : α) => x * c⁻¹

theorem map_mul_left_nhds₀ {G₀ : Type u_3} [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] {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} [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] {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} [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] {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} [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] {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} [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] {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} [TopologicalSpace G₀] [GroupWithZero G₀] [ContinuousMul G₀] (h : Filter.Tendsto Inv.inv (nhds 1) (nhds 1)) : HasContinuousInv₀ G₀

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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : ContinuousAt (fun (x : G₀) => x ^ m) x

theorem continuousOn_zpow₀ {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] (m : ℤ) : ContinuousOn (fun (x : G₀) => x ^ m) {0}ᶜ

theorem Filter.Tendsto.zpow₀ {α : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {f : α → G₀} {l : Filter α} {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} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {X : Type u_4} [TopologicalSpace X] {a : X} {f : X → G₀} (hf : ContinuousAt f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) : ContinuousAt (fun (x : X) => f x ^ m) a

theorem ContinuousWithinAt.zpow₀ {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {X : Type u_4} [TopologicalSpace X] {a : X} {s : Set X} {f : X → G₀} (hf : ContinuousWithinAt f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) : ContinuousWithinAt (fun (x : X) => f x ^ m) s a

theorem ContinuousOn.zpow₀ {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {X : Type u_4} [TopologicalSpace X] {s : Set X} {f : X → G₀} (hf : ContinuousOn f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) : ContinuousOn (fun (x : X) => f x ^ m) s

theorem Continuous.zpow₀ {G₀ : Type u_3} [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] [ContinuousMul G₀] {X : Type u_4} [TopologicalSpace X] {f : X → G₀} (hf : Continuous f) (m : ℤ) (h0 : ∀ (a : X), f a ≠ 0 ∨ 0 ≤ m) : Continuous fun (x : X) => f x ^ m