ContinuousAt.comp_div_cases
theorem ContinuousAt.comp_div_cases :
∀ {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
[inst_2 : HasContinuousInv₀ G₀] [inst_3 : ContinuousMul G₀] [inst_4 : TopologicalSpace α]
[inst_5 : TopologicalSpace β] {a : α} {f g : α → G₀} (h : α → G₀ → β),
ContinuousAt f a →
ContinuousAt g a →
(g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)) →
(g a = 0 → Filter.Tendsto (↿h) (nhds a ×ˢ ⊤) (nhds (h a 0))) → ContinuousAt (fun x => h x (f x / g x)) a
The theorem `ContinuousAt.comp_div_cases` states that for every function `f/g` where `g` can possibly be zero at a point `a` in a topological space, we can still ensure that a composite function `h` which operates on `x` and `f x / g x`, remains continuous at `a`. This condition is fulfilled if: when `g a ≠ 0`, `h` is continuous at the pair `(a, f a / g a)`; and when `g a = 0`, `h` has a limit at `a` with no information about the second component of its argument (indicated by the top filter `⊤`). This theorem is especially useful when working with uniform spaces and is characterized by the helper lemma `tendsto_prod_top_iff`.
More concisely: If a function `h : X × ℝ → Y` is continuous at every point `(a, f a/g a)` where `g(a) ≠ 0` and has a limit as `(x, y)` approaches `(a, f a/0)`, then `h(x, f x/g x)` is continuous at `a` in the uniform space setting.
|
HasContinuousInv₀.of_nhds_one
theorem HasContinuousInv₀.of_nhds_one :
∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [inst_2 : ContinuousMul G₀],
Filter.Tendsto Inv.inv (nhds 1) (nhds 1) → HasContinuousInv₀ G₀
This theorem states that for any type `G₀` which has a topology (i.e., `G₀` is a topological space), a group structure with zero, and a continuous multiplication operation, if the function which maps each element to its inverse is continuous at one (i.e., the preimage of any neighborhood of one under this function is a neighborhood of one), then the inverse operation is continuous at every unit in `G₀`. This result holds in the context of topological groups with zero, and is a property of the topology and group structure of `G₀`.
More concisely: In a topological group with identity and continuous multiplication, if the function mapping each element to its inverse is continuous at the identity, then the inverse operation is continuous at every unit.
|
Filter.Tendsto.div_const
theorem Filter.Tendsto.div_const :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [inst_2 : ContinuousMul G₀]
{f : α → G₀} {l : Filter α} {x : G₀},
Filter.Tendsto f l (nhds x) → ∀ (y : G₀), Filter.Tendsto (fun a => f a / y) l (nhds (x / y))
The theorem `Filter.Tendsto.div_const` states that for any type `α`, for any `G₀` which is a division and inversion monoid (essentially a structure with multiplication, division, and an inverse operation), and which is also a topological space with continuous multiplication. Given a function `f` from `α` to `G₀`, a filter `l` in `α`, and an element `x` in `G₀`, if `f` tends to `x` with respect to the filter `l` (i.e., for every neighborhood of `x`, the pre-image of the neighborhood under `f` is within the filter `l`), then for any element `y` in `G₀`, the function which maps `a` in `α` to `f(a)/y` also tends to `x/y` with respect to the same filter `l`. This essentially means if `f` converges to `x` then `f` divided by a constant `y` converges to `x/y`.
More concisely: If `f : α → G₀` tends to `x` in `G₀` with respect to filter `l` in `α`, then the function `g(a) = f(a) / y` tends to `x / y` in `G₀` with respect to the same filter `l`.
|
Continuous.comp_div_cases
theorem Continuous.comp_div_cases :
∀ {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
[inst_2 : HasContinuousInv₀ G₀] [inst_3 : ContinuousMul G₀] [inst_4 : TopologicalSpace α]
[inst_5 : TopologicalSpace β] {f g : α → G₀} (h : α → G₀ → β),
Continuous f →
Continuous g →
(∀ (a : α), g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)) →
(∀ (a : α), g a = 0 → Filter.Tendsto (↿h) (nhds a ×ˢ ⊤) (nhds (h a 0))) →
Continuous fun x => h x (f x / g x)
The theorem `Continuous.comp_div_cases` states that for all types `α`, `β`, and `G₀`, where `G₀` is a group with zero and `α` and `β` are topological spaces, and given functions `f` and `g` from `α` to `G₀` and a function `h` from `α` and `G₀` to `β` that are continuous, the function `h x (f x / g x)` is continuous under certain conditions, even if `g x` is sometimes `0`. The conditions are that for all `a` in `α`, if `g a` is not `0`, then `h` is continuous at `(a, f a / g a)`, and if `g a` is `0`, then `h` has a limit at `a` in the product filter of the neighborhood filter at `a` and the filter of all sets.
More concisely: Given continuous functions `f: α → G₀`, `g: α → G₀` and `h: α × G₀ → β`, if for all `a in α` where `g a ≠ 0`, `h` is continuous at `(a, f a / g a)`, and `h` has a limit at `a` in the product filter when `g a = 0`, then the function `x ↦ h x (f x / g x)` is continuous from `α` to `β`.
|
ContinuousOn.inv₀
theorem ContinuousOn.inv₀ :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀]
[inst_3 : HasContinuousInv₀ G₀] {f : α → G₀} {s : Set α} [inst_4 : TopologicalSpace α],
ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → ContinuousOn (fun x => (f x)⁻¹) s
The theorem `ContinuousOn.inv₀` states that, for any type `α` and a type `G₀` with a zero element, an inversion operation, and a topology, if `f` is a function from `α` to `G₀` and `s` is a subset of `α`, then if `f` is continuous on `s` and for all `x` in `s`, `f(x)` is not zero, it implies that the function `(f x)⁻¹`, which is the inverse of `f(x)`, is also continuous on `s`. Here continuity at a point and continuous inversion operations are understood with respect to the topology of `G₀` and the topology of `α`. This is a statement about the preservation of continuity under the operation of taking reciprocals for non-zero values in topological spaces.
More concisely: If `f` is a continuous function from `α` to a topological space `G₀` with a zero element and inversion operation, such that `f(x)` is never zero for `x` in `s`, then the inverse function `(f x)⁻¹` is also continuous on `s`.
|
Filter.Tendsto.inv₀
theorem Filter.Tendsto.inv₀ :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀]
[inst_3 : HasContinuousInv₀ G₀] {l : Filter α} {f : α → G₀} {a : G₀},
Filter.Tendsto f l (nhds a) → a ≠ 0 → Filter.Tendsto (fun x => (f x)⁻¹) l (nhds a⁻¹)
This theorem, named `Filter.Tendsto.inv₀`, states that if a function `f` converging to a non-zero value `a` under some filter `l`, then the function that is the pointwise inverse of `f` also converges under the same filter, but to the inverse of `a`. This is valid in a topological space that supports inversion and zero, and where inversion is a continuous operation. Note that this theorem is named `Filter.Tendsto.inv₀` and not `Filter.Tendsto.inv`, because the latter name is already taken for a theorem about multiplicative topological groups.
More concisely: If a function `f` converges to a non-zero value `a` under filter `l` in a topological space where inversion is continuous, then the pointwise inverse of `f` converges to the inverse of `a` under filter `l`.
|
ContinuousAt.div
theorem ContinuousAt.div :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
[inst_2 : HasContinuousInv₀ G₀] [inst_3 : ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α] {a : α},
ContinuousAt f a → ContinuousAt g a → g a ≠ 0 → ContinuousAt (f / g) a
This theorem states that for any point `a` in a topological space `α` and two functions `f` and `g` from `α` to a topological group with zero `G₀` (a group with zero that is also a topological space where the inversion and multiplication operations are continuous), if `f` and `g` are both continuous at the point `a` and `g` is nonzero at `a`, then the function that maps `x` to `f(x) / g(x)` is also continuous at `a`.
More concisely: If `f` and `g` are continuous functions from a topological space `α` to a topological group `G₀` with zero, where `g(a) ≠ 0` for some point `a` in `α`, then the function `x => f(x) / g(x)` is continuous at `a`.
|
continuousAt_zpow₀
theorem continuousAt_zpow₀ :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [inst_2 : HasContinuousInv₀ G₀]
[inst_3 : ContinuousMul G₀] (x : G₀) (m : ℤ), x ≠ 0 ∨ 0 ≤ m → ContinuousAt (fun x => x ^ m) x
The theorem `continuousAt_zpow₀` states that for any group with zero `G₀` which is also a topological space, and with continuous inverse zero and continuous multiplication, for any element `x` of this group and any integer `m`, if `x` is not equal to zero or `m` is nonnegative (i.e., `m` is zero or a positive integer), then the function that maps `x` to `x ^ m` is continuous at `x`. In other words, as `x` tends to a particular point in the topological space, `x ^ m` also tends to the corresponding point, preserving the continuity of the power function in this topological group under these conditions.
More concisely: For any commutative topological group with zero `G₀` endowed with a continuous multiplication and inversores zero, the `m`th power function is continuous on non-zero elements for any non-negative integer `m`.
|
Units.embedding_val₀
theorem Units.embedding_val₀ :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [inst_2 : HasContinuousInv₀ G₀],
Embedding Units.val
The theorem `Units.embedding_val₀` states that if `G₀` is a topological group with zero (i.e., a group with zero and a topology such that the group operations are continuous), and the function `x ↦ x⁻¹` is continuous at all nonzero points, then the coercion function from the group of units `G₀ˣ` to `G₀` is a topological embedding. In other words, there is a structure-preserving map from the nonzero elements of the group to the group itself, which also preserves the topological structure.
More concisely: If `G₀` is a topological group with a continuous inverse operation on nonzero elements, then the coercion function from `G₀ˣ` to `G₀` is a topological embedding.
|
Filter.Tendsto.zpow₀
theorem Filter.Tendsto.zpow₀ :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
[inst_2 : HasContinuousInv₀ G₀] [inst_3 : ContinuousMul G₀] {f : α → G₀} {l : Filter α} {a : G₀},
Filter.Tendsto f l (nhds a) → ∀ (m : ℤ), a ≠ 0 ∨ 0 ≤ m → Filter.Tendsto (fun x => f x ^ m) l (nhds (a ^ m))
This theorem states that for any type `α` and a type `G₀` equipped with a group structure with zero, a topology, continuous inversion, and continuous multiplication, given a function `f` from `α` to `G₀`, and a filter `l` on `α`, and an element `a` of `G₀`, if `f` tends towards `a` with respect to the filter `l` and the neighborhood filter at `a`, then for any integer `m`, if `a` is not zero or `m` is nonnegative, the function that raises `f` to the power of `m` also tends towards `a` raised to the power of `m` with respect to the filter `l` and the neighborhood filter at `a^m`.
In mathematical terms, it states that if \(\lim_{x\to l} f(x) = a\), either `a` is nonzero or `m` is nonnegative, then \(\lim_{x\to l} f(x)^m = a^m\). This theorem is basically saying that the limit of a power is the power of the limit, under certain conditions.
More concisely: If `f` is a continuous function from a topological space `α` to a group `G₀` with zero and multiplication, and `a` is a nonzero limit of `f` with respect to filter `l`, then `a^m` is the limit of `f^m` with respect to `l` for any nonnegative integer `m`.
|
ContinuousOn.div
theorem ContinuousOn.div :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
[inst_2 : HasContinuousInv₀ G₀] [inst_3 : ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α]
{s : Set α}, ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, g x ≠ 0) → ContinuousOn (f / g) s
The theorem `ContinuousOn.div` states that for any type `α`, and `G₀` which is a group with zero and a topological space that has continuous inversion and multiplication, if we have two functions `f` and `g` from `α` to `G₀` where `g` is never zero on a set `s`, and if both `f` and `g` are continuous on `s`, then the function that maps each element of `s` to the quotient of `f` and `g` at that point is also continuous on `s`. In other words, the division of two continuous functions is continuous, provided the denominator function is never zero.
More concisely: If `f` and `g` are continuous functions from a set `s` to a group `G₀` with zero and topology having continuous inversion and multiplication, where `g` is never zero on `s`, then the function that maps each point in `s` to the quotient of `f` and `g` at that point is continuous on `s`.
|
Continuous.inv₀
theorem Continuous.inv₀ :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀]
[inst_3 : HasContinuousInv₀ G₀] {f : α → G₀} [inst_4 : TopologicalSpace α],
Continuous f → (∀ (x : α), f x ≠ 0) → Continuous fun x => (f x)⁻¹
This theorem states that for any type `α`, and a type `G₀` that has a structure of a topological space, a zero element and an inverse operation, if a function `f` from `α` to `G₀` is continuous and never equals zero, then the function that maps `x` to the inverse of `f(x)` is also continuous. This is under the condition that the inverse operation is continuous at every non-zero point in `G₀`.
More concisely: If `f` is a continuous function from type `α` to a topological space `G₀` with a zero element, an inverse operation, and the inverse operation is continuous at every non-zero point, then the function that maps `x` to the inverse of `f(x)` is continuous.
|
Continuous.div_const
theorem Continuous.div_const :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [inst_2 : ContinuousMul G₀]
{f : α → G₀} [inst_3 : TopologicalSpace α], Continuous f → ∀ (y : G₀), Continuous fun x => f x / y
This theorem states that for any type `α`, any type `G₀` that is a divisional inverse monoid (a kind of algebraic structure) with a topology (a concept from topology, the study of space) and a continuous multiplication operation, and any function `f` from `α` to `G₀`, if `f` is a continuous function (a concept from calculus), then the function that maps every element `x` of type `α` to `f(x) / y` is also continuous for any `y` in `G₀`. This is a theorem about the continuity of functions under division by a constant in topological division inverse monoids.
More concisely: Given a topological divisional inverse monoid `G₀` and a continuous function `f` from type `α` to `G₀`, the function `x ↦ f(x) / y` is continuous for any fixed `y` in `G₀`.
|
Filter.Tendsto.div
theorem Filter.Tendsto.div :
∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
[inst_2 : HasContinuousInv₀ G₀] [inst_3 : ContinuousMul G₀] {f g : α → G₀} {l : Filter α} {a b : G₀},
Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → b ≠ 0 → Filter.Tendsto (f / g) l (nhds (a / b))
The theorem `Filter.Tendsto.div` asserts that for any types `α` and `G₀`, given `G₀` is a group with zero, has a topological space structure, possesses a continuous inverse, and admits continuous multiplication, if `f` and `g` are functions from `α` to `G₀`, `l` is a filter on `α`, and `a` and `b` are elements of `G₀` such that `b` is not zero, then if `f` tends to `a` and `g` tends to `b` along `l` (as defined by the `Filter.Tendsto` function), then `f / g` (the pointwise division of `f` and `g`) tends to `a / b` along `l`. In other words, the limit of the quotient of two functions is the quotient of their limits, provided the limit of the denominator function is not zero.
More concisely: If `f` and `g` are functions from a filtered space `(α, l)` to a group `G₀` with a topology, having continuous inverses and multiplication, and if `f` tends to `a` and `g` tends to `b` (not zero) along `l`, then `f / g` tends to `a / b` along `l`.
|
continuousOn_inv₀
theorem continuousOn_inv₀ :
∀ {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [inst_3 : HasContinuousInv₀ G₀],
ContinuousOn Inv.inv {0}ᶜ
This theorem states that for any type `G₀`, which is equipped with a zero element, an inversion operation, and a topological space structure, and also assuming that the inversion operation is continuous except at zero (`HasContinuousInv₀ G₀`), then the inversion function (`Inv.inv`) is continuous on the set of all elements of `G₀` excluding zero (`{0}ᶜ`). In simpler terms, if you have a space where you can flip elements around zero, and this flipping operation is continuous except at zero, then this flipping operation is continuous everywhere except at zero.
More concisely: If `G₀` is a topological space with a zero element, an inversion operation, and `HasContinuousInv₀ G₀`, then the inversion function `Inv.inv` is continuous on `G₀ \ {0}`.
|
HasContinuousInv₀.continuousAt_inv₀
theorem HasContinuousInv₀.continuousAt_inv₀ :
∀ {G₀ : Type u_4} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [self : HasContinuousInv₀ G₀]
⦃x : G₀⦄, x ≠ 0 → ContinuousAt Inv.inv x
The theorem `HasContinuousInv₀.continuousAt_inv₀` states that for all nonzero elements `x` of a type `G₀` that has an inversion operation `Inv.inv` and a topological space structure, the function that maps `x` to its inverse `x⁻¹` is continuous at `x`. In other words, as points in the topological space `G₀` get arbitrarily close to `x`, their inverses also get arbitrarily close to `x⁻¹`, provided that `x` is not the zero element of `G₀`. This theorem assumes that `G₀` has a property `HasContinuousInv₀`, which typically means that the inversion operation is continuous at every nonzero point.
More concisely: For any nonzero element `x` in a topological space `G₀` with continuous inversion operation, the function that maps `x` to its inverse is continuous at `x`.
|