Mathlib.Topology.Algebra.GroupWithZero

Module docstring

{"# 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 IsTopologicalGroups. 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. ","### 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. ","### 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. ","### Left and right multiplication as homeomorphisms "}

Filter.Tendsto.div_const theorem

{x : G₀} (hf : Tendsto f l (𝓝 x)) (y : G₀) : Tendsto (fun a => f a / y) l (𝓝 (x / y))

Full source

theorem Filter.Tendsto.div_const {x : G₀} (hf : Tendsto f l (𝓝 x)) (y : G₀) :
    Tendsto (fun a => f a / y) l (𝓝 (x / y)) := by
  simpa only [div_eq_mul_inv] using hf.mul tendsto_const_nhds

Continuity of Division by Constant in Group with Zero

Informal description

Let $G₀$ be a group with zero and continuous multiplication. For any function $f$ tending to a limit $x$ in $G₀$ along a filter $l$, and for any constant $y \in G₀$, the function $a \mapsto f(a)/y$ tends to $x/y$ along the same filter $l$.

ContinuousAt.div_const theorem

{a : α} (hf : ContinuousAt f a) (y : G₀) : ContinuousAt (fun x => f x / y) a

Full source

nonrec theorem ContinuousAt.div_const {a : α} (hf : ContinuousAt f a) (y : G₀) :
    ContinuousAt (fun x => f x / y) a :=
  hf.div_const y

Continuity of Division by Constant at a Point in Group with Zero

Informal description

Let $G₀$ be a group with zero and continuous multiplication. If a function $f$ is continuous at a point $a$ in its domain, then for any constant $y \in G₀$, the function $x \mapsto f(x) / y$ is also continuous at $a$.

ContinuousWithinAt.div_const theorem

{a} (hf : ContinuousWithinAt f s a) (y : G₀) : ContinuousWithinAt (fun x => f x / y) s a

Full source

nonrec theorem ContinuousWithinAt.div_const {a} (hf : ContinuousWithinAt f s a) (y : G₀) :
    ContinuousWithinAt (fun x => f x / y) s a :=
  hf.div_const _

Continuity Within a Subset of Division by a Constant

Informal description

Let $G₀$ be a group with zero and continuous multiplication. If a function $f$ is continuous within a subset $s$ at a point $a$, then for any constant $y \in G₀$, the function $x \mapsto f(x) / y$ is also continuous within $s$ at $a$.

ContinuousOn.div_const theorem

(hf : ContinuousOn f s) (y : G₀) : ContinuousOn (fun x => f x / y) s

Full source

theorem ContinuousOn.div_const (hf : ContinuousOn f s) (y : G₀) :
    ContinuousOn (fun x => f x / y) s := by
  simpa only [div_eq_mul_inv] using hf.mul continuousOn_const

Continuity of Division by a Constant on a Subset

Informal description

Let $G₀$ be a group with zero and a topological space. If a function $f$ is continuous on a subset $s$ of its domain, then for any element $y \in G₀$, the function $x \mapsto f(x) / y$ is also continuous on $s$.

Continuous.div_const theorem

(hf : Continuous f) (y : G₀) : Continuous fun x => f x / y

Full source

@[continuity, fun_prop]
theorem Continuous.div_const (hf : Continuous f) (y : G₀) : Continuous fun x => f x / y := by
  simpa only [div_eq_mul_inv] using hf.mul continuous_const

Continuity of Division by a Constant

Informal description

Let $G₀$ be a topological space with a zero element and a division operation, and let $f$ be a continuous function from a topological space to $G₀$. Then for any $y \in G₀$, the function $x \mapsto f(x) / y$ is continuous.

HasContinuousInv₀ structure

(G₀ : Type*) [Zero G₀] [Inv G₀] [TopologicalSpace G₀]

Full source

/-- A type with `0` and `Inv` such that `fun x ↦ x⁻¹` is continuous at all nonzero points. Any
normed (semi)field has this property. -/
class HasContinuousInv₀ (G₀ : Type*) [Zero G₀] [Inv G₀] [TopologicalSpace G₀] : Prop where
  /-- The map `fun x ↦ x⁻¹` is continuous at all nonzero points. -/
  continuousAt_inv₀ : ∀ ⦃x : G₀⦄, x ≠ 0 → ContinuousAt Inv.inv x

Type with Continuous Inversion at Nonzero Points

Informal description

A structure representing a type `G₀` equipped with zero and an inversion operation, where the inversion operation is continuous at all nonzero points. This property is satisfied by any normed (semi)field.

tendsto_inv₀ theorem

{x : G₀} (hx : x ≠ 0) : Tendsto Inv.inv (𝓝 x) (𝓝 x⁻¹)

Full source

theorem tendsto_inv₀ {x : G₀} (hx : x ≠ 0) : Tendsto Inv.inv (𝓝 x) (𝓝 x⁻¹) :=
  continuousAt_inv₀ hx

Continuity of Inversion at Nonzero Points

Informal description

Let $G₀$ be a topological space with zero and inversion operations, where inversion is continuous at all nonzero points. For any nonzero element $x \in G₀$, the inversion function $x \mapsto x^{-1}$ is continuous at $x$, meaning that as $y$ approaches $x$, $y^{-1}$ approaches $x^{-1}$.

continuousOn_inv₀ theorem

: ContinuousOn (Inv.inv : G₀ → G₀) {0}ᶜ

Full source

theorem continuousOn_inv₀ : ContinuousOn (Inv.inv : G₀ → G₀) {0}{0}ᶜ := fun _x hx =>
  (continuousAt_inv₀ hx).continuousWithinAt

Continuity of Inversion on Nonzero Points

Informal description

The inversion function $x \mapsto x^{-1}$ is continuous on the complement of $\{0\}$ in a topological group with zero $G₀$, i.e., it is continuous at every nonzero point of $G₀$.

Filter.Tendsto.inv₀ theorem

{a : G₀} (hf : Tendsto f l (𝓝 a)) (ha : a ≠ 0) : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)

Full source

/-- 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 Filter.Tendsto.inv₀ {a : G₀} (hf : Tendsto f l (𝓝 a)) (ha : a ≠ 0) :
    Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹) :=
  (tendsto_inv₀ ha).comp hf

Limit of Inverses at Nonzero Points: $\lim_{x \to l} (f(x))^{-1} = (\lim_{x \to l} f(x))^{-1}$ when $\lim_{x \to l} f(x) \neq 0$

Informal description

Let $G₀$ be a topological space with zero and inversion operations, where inversion is continuous at all nonzero points. Let $f$ be a function such that $f(x)$ tends to a nonzero limit $a$ as $x$ approaches some limit point in the filter $l$. Then the function $x \mapsto (f(x))^{-1}$ tends to $a^{-1}$ in the same filter.

ContinuousWithinAt.inv₀ theorem

(hf : ContinuousWithinAt f s a) (ha : f a ≠ 0) : ContinuousWithinAt (fun x => (f x)⁻¹) s a

Full source

nonrec theorem ContinuousWithinAt.inv₀ (hf : ContinuousWithinAt f s a) (ha : f a ≠ 0) :
    ContinuousWithinAt (fun x => (f x)⁻¹) s a :=
  hf.inv₀ ha

Continuity of Inversion Within a Subset at Nonzero Points: $(f(x))^{-1}$ is continuous within $s$ at $a$ when $f$ is continuous within $s$ at $a$ and $f(a) \neq 0$

Informal description

Let $G₀$ be a topological space with zero and inversion operations, where inversion is continuous at all nonzero points. If a function $f \colon G₀ \to G₀$ is continuous within a subset $s$ at a point $a$ and $f(a) \neq 0$, then the function $x \mapsto (f(x))^{-1}$ is also continuous within $s$ at $a$.

ContinuousAt.inv₀ theorem

(hf : ContinuousAt f a) (ha : f a ≠ 0) : ContinuousAt (fun x => (f x)⁻¹) a

Full source

@[fun_prop]
nonrec theorem ContinuousAt.inv₀ (hf : ContinuousAt f a) (ha : f a ≠ 0) :
    ContinuousAt (fun x => (f x)⁻¹) a :=
  hf.inv₀ ha

Continuity of Inversion at Nonzero Points: $(f(x))^{-1}$ is continuous at $a$ when $f$ is continuous at $a$ and $f(a) \neq 0$

Informal description

Let $G₀$ be a topological space with zero and inversion operations, where inversion is continuous at all nonzero points. If a function $f$ is continuous at a point $a$ and $f(a) \neq 0$, then the function $x \mapsto (f(x))^{-1}$ is also continuous at $a$.

Continuous.inv₀ theorem

(hf : Continuous f) (h0 : ∀ x, f x ≠ 0) : Continuous fun x => (f x)⁻¹

Full source

@[continuity, fun_prop]
theorem Continuous.inv₀ (hf : Continuous f) (h0 : ∀ x, f x ≠ 0) : Continuous fun x => (f x)⁻¹ :=
  continuous_iff_continuousAt.2 fun x => (hf.tendsto x).inv₀ (h0 x)

Continuity of Inversion for Nonzero Continuous Functions: $(f(x))^{-1}$ is continuous when $f$ is continuous and nowhere zero

Informal description

Let $G₀$ be a topological space with zero and inversion operations, where inversion is continuous at all nonzero points. If a function $f \colon G₀ \to G₀$ is continuous and $f(x) \neq 0$ for all $x \in G₀$, then the function $x \mapsto (f(x))^{-1}$ is also continuous.

ContinuousOn.inv₀ theorem

(hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContinuousOn (fun x => (f x)⁻¹) s

Full source

@[fun_prop]
theorem ContinuousOn.inv₀ (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
    ContinuousOn (fun x => (f x)⁻¹) s := fun x hx => (hf x hx).inv₀ (h0 x hx)

Continuity of Inversion on a Subset for Nonzero Continuous Functions: $(f(x))^{-1}$ is continuous on $s$ when $f$ is continuous on $s$ and nowhere zero on $s$

Informal description

Let $G₀$ be a topological space with zero and inversion operations, where inversion is continuous at all nonzero points. If a function $f \colon G₀ \to G₀$ is continuous on a subset $s \subseteq G₀$ and $f(x) \neq 0$ for all $x \in s$, then the function $x \mapsto (f(x))^{-1}$ is also continuous on $s$.

Units.isEmbedding_val₀ theorem

[GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] : IsEmbedding (val : G₀ˣ → G₀)

Full source

/-- 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 Units.isEmbedding_val₀ [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] :
    IsEmbedding (val : G₀ˣ → G₀) :=
  embedding_val_mk <| (continuousOn_inv₀ (G₀ := G₀)).mono fun _ ↦ IsUnit.ne_zero

Topological Embedding of Units in a Group with Zero

Informal description

Let $G₀$ be a topological group with zero such that the inversion map $x \mapsto x^{-1}$ is continuous at all nonzero points. Then the canonical embedding of the units $G₀^×$ into $G₀$ is a topological embedding.

nhds_inv₀ theorem

(hx : x ≠ 0) : 𝓝 x⁻¹ = (𝓝 x)⁻¹

Full source

lemma nhds_inv₀ (hx : x ≠ 0) : 𝓝 x⁻¹ = (𝓝 x)⁻¹ := by
  refine le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)
  simpa only [inv_inv] using tendsto_inv₀ (inv_ne_zero hx)

Neighborhood Filter of Inverse Equals Preimage of Neighborhood Filter at Nonzero Points

Informal description

Let $G_0$ be a topological space equipped with zero and an inversion operation, where inversion is continuous at all nonzero points. For any nonzero element $x \in G_0$, the neighborhood filter of $x^{-1}$ is equal to the preimage under inversion of the neighborhood filter of $x$, i.e., $\mathcal{N}(x^{-1}) = \mathcal{N}(x)^{-1}$.

tendsto_inv_iff₀ theorem

 {l : Filter α} {f : α → G₀} (hx : x ≠ 0) : Tendsto (fun x ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x)

Full source

lemma tendsto_inv_iff₀ {l : Filter α} {f : α → G₀} (hx : x ≠ 0) :
    TendstoTendsto (fun x ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x) := by
  simp only [nhds_inv₀ hx, ← Filter.comap_inv, tendsto_comap_iff, Function.comp_def, inv_inv]

Equivalence of Tendency to Inverses and Tendency to Original Points at Nonzero Elements

Informal description

Let $G_0$ be a topological space with zero and an inversion operation such that inversion is continuous at all nonzero points. For any filter $l$ on a type $\alpha$, any function $f \colon \alpha \to G_0$, and any nonzero element $x \in G_0$, the following are equivalent: 1. The function $\lambda y, (f y)^{-1}$ tends to $x^{-1}$ along the filter $l$. 2. The function $f$ tends to $x$ along the filter $l$.

Filter.Tendsto.div theorem

 {l : Filter α} {a b : G₀} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) (hy : b ≠ 0) :
  Tendsto (f / g) l (𝓝 (a / b))

Full source

theorem Filter.Tendsto.div {l : Filter α} {a b : G₀} (hf : Tendsto f l (𝓝 a))
    (hg : Tendsto g l (𝓝 b)) (hy : b ≠ 0) : Tendsto (f / g) l (𝓝 (a / b)) := by
  simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ hy)

Limit of Quotient: $\lim_{x \to l} \frac{f(x)}{g(x)} = \frac{\lim_{x \to l} f(x)}{\lim_{x \to l} g(x)}$ when $\lim_{x \to l} g(x) \neq 0$

Informal description

Let $G₀$ be a topological space with zero and division operations, where inversion is continuous at all nonzero points. Let $f$ and $g$ be functions such that $f(x)$ tends to $a$ and $g(x)$ tends to $b \neq 0$ as $x$ approaches some limit point in the filter $l$. Then the function $x \mapsto f(x) / g(x)$ tends to $a / b$ in the same filter.

Filter.tendsto_mul_iff_of_ne_zero theorem

 [T1Space G₀] {f g : α → G₀} {l : Filter α} {x y : G₀} (hg : Tendsto g l (𝓝 y)) (hy : y ≠ 0) :
  Tendsto (fun n => f n * g n) l (𝓝 <| x * y) ↔ Tendsto f l (𝓝 x)

Full source

theorem Filter.tendsto_mul_iff_of_ne_zero [T1Space G₀] {f g : α → G₀} {l : Filter α} {x y : G₀}
    (hg : Tendsto g l (𝓝 y)) (hy : y ≠ 0) :
    TendstoTendsto (fun n => f n * g n) l (𝓝 <| x * y) ↔ Tendsto f l (𝓝 x) := by
  refine ⟨fun hfg => ?_, fun hf => hf.mul hg⟩
  rw [← mul_div_cancel_right₀ x hy]
  refine Tendsto.congr' ?_ (hfg.div hg hy)
  exact (hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

Limit of Product Equals Product of Limits at Nonzero Points in $T_1$ Space

Informal description

Let $G₀$ be a topological space with zero and multiplication, where inversion is continuous at all nonzero points and the space is $T_1$. Let $f, g \colon \alpha \to G₀$ be functions, $l$ a filter on $\alpha$, and $x, y \in G₀$ with $y \neq 0$. If $g$ tends to $y$ along $l$, then the function $n \mapsto f(n) * g(n)$ tends to $x * y$ along $l$ if and only if $f$ tends to $x$ along $l$.

ContinuousWithinAt.div theorem

(hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) (h₀ : g a ≠ 0) : ContinuousWithinAt (f / g) s a

Full source

nonrec theorem ContinuousWithinAt.div (hf : ContinuousWithinAt f s a)
    (hg : ContinuousWithinAt g s a) (h₀ : g a ≠ 0) : ContinuousWithinAt (f / g) s a :=
  hf.div hg h₀

Continuity of Quotient within a Subset at a Point

Informal description

Let $G₀$ be a topological space with zero and division operations, where inversion is continuous at all nonzero points. Let $f$ and $g$ be functions from a topological space to $G₀$, and let $s$ be a subset of the domain. If $f$ is continuous within $s$ at a point $a$, $g$ is continuous within $s$ at $a$, and $g(a) \neq 0$, then the function $f/g$ is continuous within $s$ at $a$.

ContinuousOn.div theorem

(hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContinuousOn (f / g) s

Full source

theorem ContinuousOn.div (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
    ContinuousOn (f / g) s := fun x hx => (hf x hx).div (hg x hx) (h₀ x hx)

Continuity of Quotient on a Subset with Nonzero Denominator

Informal description

Let $G₀$ be a topological space with zero and division operations, where inversion is continuous at all nonzero points. Let $f$ and $g$ be functions from a topological space to $G₀$, and let $s$ be a subset of the domain. If $f$ and $g$ are continuous on $s$, and $g(x) \neq 0$ for all $x \in s$, then the function $f/g$ is continuous on $s$.

ContinuousAt.div theorem

(hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) : ContinuousAt (f / g) a

Full source

/-- Continuity at a point of the result of dividing two functions continuous at that point, where
the denominator is nonzero. -/
nonrec theorem ContinuousAt.div (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) :
    ContinuousAt (f / g) a :=
  hf.div hg h₀

Continuity of Quotient at a Point: $(f/g)$ is Continuous at $a$ when $g(a) \neq 0$

Informal description

Let $G₀$ be a topological space with zero and division operations, where inversion is continuous at all nonzero points. If $f$ and $g$ are functions continuous at a point $a$, and $g(a) \neq 0$, then the function $x \mapsto f(x) / g(x)$ is continuous at $a$.

Continuous.div theorem

(hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) : Continuous (f / g)

Full source

@[continuity]
theorem Continuous.div (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) :
    Continuous (f / g) := by simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Continuity of Quotient of Continuous Functions with Nonzero Denominator

Informal description

Let $G₀$ be a topological space with continuous division and inversion operations. If $f, g \colon G₀ \to G₀$ are continuous functions and $g(x) \neq 0$ for all $x \in G₀$, then the quotient function $f/g$ defined by $(f/g)(x) = f(x)/g(x)$ is continuous.

continuousOn_div theorem

: ContinuousOn (fun p : G₀ × G₀ => p.1 / p.2) {p | p.2 ≠ 0}

Full source

theorem continuousOn_div : ContinuousOn (fun p : G₀ × G₀ => p.1 / p.2) { p | p.2 ≠ 0 } :=
  continuousOn_fst.div continuousOn_snd fun _ => id

Continuity of Division on Nonzero Denominator Subset

Informal description

The division operation $(x, y) \mapsto x / y$ is continuous on the subset $\{(x, y) \in G₀ \times G₀ \mid y \neq 0\}$ of the product space $G₀ \times G₀$, where $G₀$ is a topological group with zero and continuous inversion at nonzero points.

Continuous.div₀ theorem

(hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) : Continuous (fun x => f x / g x)

Full source

@[fun_prop]
theorem Continuous.div₀ (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) :
    Continuous (fun x => f x / g x) := by
  simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Continuity of Division for Nonzero Denominator Functions

Informal description

Let $G₀$ be a topological group with zero where inversion is continuous at all nonzero points. If $f, g \colon G₀ \to G₀$ are continuous functions and $g(x) \neq 0$ for all $x \in G₀$, then the function $x \mapsto \frac{f(x)}{g(x)}$ is continuous.

ContinuousAt.div₀ theorem

(hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) : ContinuousAt (fun x => f x / g x) a

Full source

@[fun_prop]
theorem ContinuousAt.div₀ (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) :
    ContinuousAt (fun x => f x / g x) a := ContinuousAt.div hf hg h₀

Continuity of Division at a Point with Nonzero Denominator

Informal description

Let $G₀$ be a topological group with zero where inversion is continuous at all nonzero points. If $f$ and $g$ are functions continuous at a point $a \in G₀$, and $g(a) \neq 0$, then the function $x \mapsto f(x) / g(x)$ is continuous at $a$.

ContinuousOn.div₀ theorem

(hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContinuousOn (fun x => f x / g x) s

Full source

@[fun_prop]
theorem ContinuousOn.div₀ (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
    ContinuousOn (fun x => f x / g x) s := ContinuousOn.div hf hg h₀

Continuity of Division on a Subset with Nonzero Denominator

Informal description

Let $G₀$ be a topological group with zero where inversion is continuous at all nonzero points. Let $f, g \colon X \to G₀$ be functions defined on a topological space $X$, and let $s \subseteq X$. If $f$ and $g$ are continuous on $s$, and $g(x) \neq 0$ for all $x \in s$, then the function $x \mapsto f(x)/g(x)$ is continuous on $s$.

ContinuousAt.comp_div_cases theorem

 {f 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 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))) :
  ContinuousAt (fun x => h x (f x / g x)) a

Full source

/-- 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 ContinuousAt.comp_div_cases {f 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 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))) :
    ContinuousAt (fun x => h x (f x / g x)) a := by
  show ContinuousAt (↿h↿h ∘ fun x => (x, f x / g x)) a
  by_cases hga : g a = 0
  · rw [ContinuousAt]
    simp_rw [comp_apply, hga, div_zero]
    exact (h2h hga).comp (continuousAt_id.tendsto.prodMk tendsto_top)
  · fun_prop (disch := assumption)

Continuity of Composition with Division at a Point

Informal description

Let $G₀$ be a topological group with zero where inversion is continuous at all nonzero points. Let $f, g : \alpha \to G₀$ be functions continuous at a point $a \in \alpha$, and let $h : \alpha \to G₀ \to \beta$ be a function such that: 1. If $g(a) \neq 0$, then $h$ is continuous at $(a, f(a)/g(a))$; 2. If $g(a) = 0$, then $h(x,y)$ tends to $h(a,0)$ as $x$ tends to $a$ (with no condition on $y$). Then the function $x \mapsto h(x, f(x)/g(x))$ is continuous at $a$.

Continuous.comp_div_cases theorem

 {f 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 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))) :
  Continuous fun x => h x (f x / g x)

Full source

/-- `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`. -/
theorem Continuous.comp_div_cases {f 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 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))) :
    Continuous fun x => h x (f x / g x) :=
  continuous_iff_continuousAt.mpr fun a =>
    hf.continuousAt.comp_div_cases _ hg.continuousAt (hh a) (h2h a)

Continuity of Composition with Division in a Topological Group with Zero

Informal description

Let $G₀$ be a topological group with zero where inversion is continuous at all nonzero points. Let $f, g \colon \alpha \to G₀$ be continuous functions, and let $h \colon \alpha \to G₀ \to \beta$ be a function such that: 1. For every $a \in \alpha$ with $g(a) \neq 0$, the function $h$ is continuous at $(a, f(a)/g(a))$; 2. For every $a \in \alpha$ with $g(a) = 0$, the function $h(x,y)$ tends to $h(a,0)$ as $x$ tends to $a$ (with no condition on $y$). Then the function $x \mapsto h(x, f(x)/g(x))$ is continuous on $\alpha$.

Homeomorph.mulLeft₀ definition

(c : α) (hc : c ≠ 0) : α ≃ₜ α

Full source

/-- Left multiplication by a nonzero element in a `GroupWithZero` with continuous multiplication
is a homeomorphism of the underlying type. -/
protected def mulLeft₀ (c : α) (hc : c ≠ 0) : α ≃ₜ α :=
  { Equiv.mulLeft₀ c hc with
    continuous_toFun := continuous_mul_left _
    continuous_invFun := continuous_mul_left _ }

Homeomorphism of left multiplication by a nonzero element

Informal description

For a topological group with zero $\alpha$ and a nonzero element $c \in \alpha$, the left multiplication map $x \mapsto c \cdot x$ is a homeomorphism of $\alpha$ onto itself. This means it is a continuous bijection with a continuous inverse.

Homeomorph.mulRight₀ definition

(c : α) (hc : c ≠ 0) : α ≃ₜ α

Full source

/-- Right multiplication by a nonzero element in a `GroupWithZero` with continuous multiplication
is a homeomorphism of the underlying type. -/
protected def mulRight₀ (c : α) (hc : c ≠ 0) : α ≃ₜ α :=
  { Equiv.mulRight₀ c hc with
    continuous_toFun := continuous_mul_right _
    continuous_invFun := continuous_mul_right _ }

Right multiplication homeomorphism in a group with zero

Informal description

Given a `GroupWithZero` $\alpha$ with continuous multiplication, for any nonzero element $c \in \alpha$, the right multiplication map $x \mapsto x \cdot c$ is a homeomorphism of $\alpha$.

Homeomorph.coe_mulLeft₀ theorem

(c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulLeft₀ c hc) = (c * ·)

Full source

@[simp]
theorem coe_mulLeft₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulLeft₀ c hc) = (c * ·) :=
  rfl

Coefficient of Left Multiplication Homeomorphism by Nonzero Element

Informal description

For a topological group with zero $\alpha$ and a nonzero element $c \in \alpha$, the homeomorphism $\text{mulLeft}_0\,c\,hc$ is given by the function $x \mapsto c \cdot x$.

Homeomorph.mulLeft₀_symm_apply theorem

(c : α) (hc : c ≠ 0) : ((Homeomorph.mulLeft₀ c hc).symm : α → α) = (c⁻¹ * ·)

Full source

@[simp]
theorem mulLeft₀_symm_apply (c : α) (hc : c ≠ 0) :
    ((Homeomorph.mulLeft₀ c hc).symm : α → α) = (c⁻¹ * ·) :=
  rfl

Inverse of Left Multiplication Homeomorphism by Nonzero Element

Informal description

For a topological group with zero $\alpha$ and a nonzero element $c \in \alpha$, the inverse of the left multiplication homeomorphism $x \mapsto c \cdot x$ is given by $x \mapsto c^{-1} \cdot x$.

Homeomorph.coe_mulRight₀ theorem

(c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulRight₀ c hc) = (· * c)

Full source

@[simp]
theorem coe_mulRight₀ (c : α) (hc : c ≠ 0) : ⇑(Homeomorph.mulRight₀ c hc) = (· * c) :=
  rfl

Right Multiplication Homeomorphism Function in a Group with Zero

Informal description

For any nonzero element $c$ in a topological group with zero $\alpha$, the underlying function of the right multiplication homeomorphism $\text{Homeomorph.mulRight₀}\ c\ hc$ is equal to the function $x \mapsto x \cdot c$.

Homeomorph.mulRight₀_symm_apply theorem

(c : α) (hc : c ≠ 0) : ((Homeomorph.mulRight₀ c hc).symm : α → α) = (· * c⁻¹)

Full source

@[simp]
theorem mulRight₀_symm_apply (c : α) (hc : c ≠ 0) :
    ((Homeomorph.mulRight₀ c hc).symm : α → α) = (· * c⁻¹) :=
  rfl

Inverse of Right Multiplication Homeomorphism in a Group with Zero

Informal description

For any nonzero element $c$ in a group with zero $\alpha$ that has continuous multiplication, the inverse of the right multiplication homeomorphism $x \mapsto x \cdot c$ is given by $x \mapsto x \cdot c^{-1}$.

map_mul_left_nhds₀ theorem

(ha : a ≠ 0) (b : G₀) : map (a * ·) (𝓝 b) = 𝓝 (a * b)

Full source

theorem map_mul_left_nhds₀ (ha : a ≠ 0) (b : G₀) : map (a * ·) (𝓝 b) = 𝓝 (a * b) :=
  (Homeomorph.mulLeft₀ a ha).map_nhds_eq b

Neighborhood filter transformation under left multiplication by a nonzero element

Informal description

For a topological group with zero $G_0$ and a nonzero element $a \in G_0$, the pushforward of the neighborhood filter $\mathcal{N}(b)$ under the left multiplication map $x \mapsto a \cdot x$ is equal to the neighborhood filter $\mathcal{N}(a \cdot b)$.

map_mul_left_nhds_one₀ theorem

(ha : a ≠ 0) : map (a * ·) (𝓝 1) = 𝓝 (a)

Full source

theorem map_mul_left_nhds_one₀ (ha : a ≠ 0) : map (a * ·) (𝓝 1) = 𝓝 (a) := by
  rw [map_mul_left_nhds₀ ha, mul_one]

Left multiplication maps identity neighborhood to neighborhood of nonzero element

Informal description

For any nonzero element $a$ in a topological group with zero $G_0$, the pushforward of the neighborhood filter of the identity element $1$ under the left multiplication map $x \mapsto a \cdot x$ is equal to the neighborhood filter of $a$.

map_mul_right_nhds₀ theorem

(ha : a ≠ 0) (b : G₀) : map (· * a) (𝓝 b) = 𝓝 (b * a)

Full source

theorem map_mul_right_nhds₀ (ha : a ≠ 0) (b : G₀) : map (· * a) (𝓝 b) = 𝓝 (b * a) :=
  (Homeomorph.mulRight₀ a ha).map_nhds_eq b

Right Multiplication Preserves Neighborhoods in a Group with Zero

Informal description

Let $G₀$ be a group with zero and continuous multiplication. For any nonzero element $a \in G₀$ and any element $b \in G₀$, the image of the neighborhood filter of $b$ under right multiplication by $a$ is equal to the neighborhood filter of $b \cdot a$.

map_mul_right_nhds_one₀ theorem

(ha : a ≠ 0) : map (· * a) (𝓝 1) = 𝓝 (a)

Full source

theorem map_mul_right_nhds_one₀ (ha : a ≠ 0) : map (· * a) (𝓝 1) = 𝓝 (a) := by
  rw [map_mul_right_nhds₀ ha, one_mul]

Right Multiplication Maps Identity Neighborhood to Neighborhood of Nonzero Element in Group with Zero

Informal description

Let $G₀$ be a group with zero and continuous multiplication. For any nonzero element $a \in G₀$, the image of the neighborhood filter of the identity element $1$ under right multiplication by $a$ is equal to the neighborhood filter of $a$.

nhds_translation_mul_inv₀ theorem

(ha : a ≠ 0) : comap (· * a⁻¹) (𝓝 1) = 𝓝 a

Full source

theorem nhds_translation_mul_inv₀ (ha : a ≠ 0) : comap (· * a⁻¹) (𝓝 1) = 𝓝 a :=
  ((Homeomorph.mulRight₀ a ha).symm.comap_nhds_eq 1).trans <| by simp

Neighborhood Filter Characterization via Right Multiplication by Inverse in Group with Zero

Informal description

For any nonzero element $a$ in a group with zero $G_0$ where the inversion operation is continuous at nonzero points, the neighborhood filter of $a$ is equal to the preimage of the neighborhood filter of $1$ under the map $x \mapsto x \cdot a^{-1}$.

HasContinuousInv₀.of_nhds_one theorem

(h : Tendsto Inv.inv (𝓝 (1 : G₀)) (𝓝 1)) : HasContinuousInv₀ G₀

Full source

/-- If a group with zero has continuous multiplication and `fun x ↦ x⁻¹` is continuous at one,
then it is continuous at any unit. -/
theorem HasContinuousInv₀.of_nhds_one (h : Tendsto Inv.inv (𝓝 (1 : G₀)) (𝓝 1)) :
    HasContinuousInv₀ G₀ where
  continuousAt_inv₀ x hx := by
    have hx' := inv_ne_zero hx
    rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx',
      tendsto_map'_iff, tendsto_comap_iff]
    simpa only [Function.comp_def, mul_inv_rev, mul_inv_cancel_right₀ hx']

Continuity of Inversion at Units from Continuity at Identity in Group with Zero

Informal description

Let $G_0$ be a group with zero and continuous multiplication. If the inversion operation $x \mapsto x^{-1}$ is continuous at the identity element $1$, then it is continuous at every unit (nonzero element) of $G_0$.

continuousAt_zpow₀ theorem

(x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : ContinuousAt (fun x => x ^ m) x

Full source

theorem continuousAt_zpow₀ (x : G₀) (m : ℤ) (h : x ≠ 0x ≠ 0 ∨ 0 ≤ m) :
    ContinuousAt (fun x => x ^ m) x := by
  rcases m with m | m
  · simpa only [Int.ofNat_eq_coe, zpow_natCast] using continuousAt_pow x m
  · simp only [zpow_negSucc]
    have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_le
    exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)

Continuity of Integer Power Function at Nonzero Points or Nonnegative Exponents

Informal description

Let $G₀$ be a group with zero where inversion is continuous at nonzero points. For any $x \in G₀$ and integer $m \in \mathbb{Z}$, the function $x \mapsto x^m$ is continuous at $x$ provided that either $x \neq 0$ or $m \geq 0$.

continuousOn_zpow₀ theorem

(m : ℤ) : ContinuousOn (fun x : G₀ => x ^ m) {0}ᶜ

Full source

theorem continuousOn_zpow₀ (m : ℤ) : ContinuousOn (fun x : G₀ => x ^ m) {0}{0}ᶜ := fun _x hx =>
  (continuousAt_zpow₀ _ _ (Or.inl hx)).continuousWithinAt

Continuity of Integer Power Function on Nonzero Elements

Informal description

For any integer $m \in \mathbb{Z}$, the function $x \mapsto x^m$ is continuous on the set of nonzero elements of a group with zero $G₀$ where inversion is continuous at nonzero points.

Filter.Tendsto.zpow₀ theorem

 {f : α → G₀} {l : Filter α} {a : G₀} (hf : Tendsto f l (𝓝 a)) (m : ℤ) (h : a ≠ 0 ∨ 0 ≤ m) :
  Tendsto (fun x => f x ^ m) l (𝓝 (a ^ m))

Full source

theorem Filter.Tendsto.zpow₀ {f : α → G₀} {l : Filter α} {a : G₀} (hf : Tendsto f l (𝓝 a)) (m : ℤ)
    (h : a ≠ 0a ≠ 0 ∨ 0 ≤ m) : Tendsto (fun x => f x ^ m) l (𝓝 (a ^ m)) :=
  (continuousAt_zpow₀ _ m h).tendsto.comp hf

Limit of Integer Power Function at Nonzero Points or Nonnegative Exponents

Informal description

Let $G₀$ be a group with zero where inversion is continuous at nonzero points. Given a function $f : \alpha \to G₀$, a filter $l$ on $\alpha$, and a point $a \in G₀$, if $f$ tends to $a$ along $l$, then for any integer $m \in \mathbb{Z}$ such that either $a \neq 0$ or $m \geq 0$, the function $x \mapsto f(x)^m$ tends to $a^m$ along $l$.

ContinuousAt.zpow₀ theorem

(hf : ContinuousAt f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) : ContinuousAt (fun x => f x ^ m) a

Full source

@[fun_prop]
nonrec theorem ContinuousAt.zpow₀ (hf : ContinuousAt f a) (m : ℤ) (h : f a ≠ 0f a ≠ 0 ∨ 0 ≤ m) :
    ContinuousAt (fun x => f x ^ m) a :=
  hf.zpow₀ m h

Continuity of Integer Power Function at a Point with Nonzero Base or Nonnegative Exponent

Informal description

Let $G₀$ be a group with zero where inversion is continuous at nonzero points. If a function $f : \alpha \to G₀$ is continuous at a point $a \in G₀$, then for any integer $m \in \mathbb{Z}$ such that either $f(a) \neq 0$ or $m \geq 0$, the function $x \mapsto f(x)^m$ is also continuous at $a$.

ContinuousWithinAt.zpow₀ theorem

(hf : ContinuousWithinAt f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) : ContinuousWithinAt (fun x => f x ^ m) s a

Full source

nonrec theorem ContinuousWithinAt.zpow₀ (hf : ContinuousWithinAt f s a) (m : ℤ)
    (h : f a ≠ 0f a ≠ 0 ∨ 0 ≤ m) : ContinuousWithinAt (fun x => f x ^ m) s a :=
  hf.zpow₀ m h

Continuity of Integer Power Function Within a Set at a Point

Informal description

Let $G₀$ be a group with zero where inversion is continuous at nonzero points. Given a function $f : \alpha \to G₀$, a set $s \subseteq \alpha$, and a point $a \in \alpha$, if $f$ is continuous within $s$ at $a$, then for any integer $m \in \mathbb{Z}$ such that either $f(a) \neq 0$ or $m \geq 0$, the function $x \mapsto f(x)^m$ is continuous within $s$ at $a$.

ContinuousOn.zpow₀ theorem

(hf : ContinuousOn f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) : ContinuousOn (fun x => f x ^ m) s

Full source

@[fun_prop]
theorem ContinuousOn.zpow₀ (hf : ContinuousOn f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) :
    ContinuousOn (fun x => f x ^ m) s := fun a ha => (hf a ha).zpow₀ m (h a ha)

Continuity of Integer Power Function on a Set with Nonzero Base or Nonnegative Exponent

Informal description

Let $G₀$ be a group with zero where inversion is continuous at nonzero points. Given a function $f \colon X \to G₀$ that is continuous on a set $s \subseteq X$, and an integer $m \in \mathbb{Z}$ such that for every $a \in s$, either $f(a) \neq 0$ or $m \geq 0$, the function $x \mapsto f(x)^m$ is continuous on $s$.

Continuous.zpow₀ theorem

(hf : Continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) : Continuous fun x => f x ^ m

Full source

@[continuity, fun_prop]
theorem Continuous.zpow₀ (hf : Continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0f a ≠ 0 ∨ 0 ≤ m) :
    Continuous fun x => f x ^ m :=
  continuous_iff_continuousAt.2 fun x => (hf.tendsto x).zpow₀ m (h0 x)

Continuity of Integer Power Function under Continuous Maps

Informal description

Let $G₀$ be a group with zero where inversion is continuous at nonzero points. Given a continuous function $f \colon X \to G₀$ and an integer $m \in \mathbb{Z}$ such that for every $a \in X$, either $f(a) \neq 0$ or $m \geq 0$, the function $x \mapsto f(x)^m$ is continuous.