Documentation

Mathlib.Topology.Algebra.GroupWithZero

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₀] :

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₀] [TopologicalSpace G₀] [self : HasContinuousInv₀ G₀] ⦃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₀] [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 : xs, 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) :
    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) :
    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₀ : xs, 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) :
    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₀ : 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} [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 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} [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 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} [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
    Instances For
      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
      Instances For
        @[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.mulLeft₀ c hc).symm = 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.mulRight₀ c hc).symm = 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

        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 : XG₀} (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 : XG₀} (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 : XG₀} (hf : ContinuousOn f s) (m : ) (h : as, 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 : XG₀} (hf : Continuous f) (m : ) (h0 : ∀ (a : X), f a 0 0 m) :
        Continuous fun (x : X) => f x ^ m