Topological group with zero #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define has_continuous_inv₀ to be a mixin typeclass a type with has_inv and
has_zero (e.g., a group_with_zero) such that λ x, x⁻¹ is continuous at all nonzero points. Any
normed (semi)field has this property. Currently the only example of has_continuous_inv₀ in
mathlib which is not a normed field is the type nnnreal (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, continuous_at, continuous_within_at, continuous_on,
and continuous. As a special case, we provide *.div_const operations that require only
group_with_zero and has_continuous_mul instances.
All lemmas about (⁻¹) use inv' in their names because lemmas without ' are used for
topological_groups. We also use ' in the typeclass name has_continuous_inv₀ for the sake of
consistency of notation.
On a group_with_zero with continuous multiplication, we also define left and right multiplication
as homeomorphisms.
A group with zero with continuous multiplication #
If G₀ is a group with zero 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, continuous_at, continuous_within_at, continuous_on, and
continuous.
- continuous_at_inv₀ : ∀ ⦃x : G₀⦄, x ≠ 0 → continuous_at has_inv.inv x
A type with 0 and has_inv such that λ x, x⁻¹ is continuous at all nonzero points. Any
normed (semi)field has this property.
Instances of this typeclass
Continuity of λ x, x⁻¹ at a non-zero point #
We define topological_group_with_zero to be a group_with_zero such that the operation x ↦ x⁻¹
is continuous at all nonzero points. In this section we prove dot-style *.inv' lemmas for
filter.tendsto, continuous_at, continuous_within_at, continuous_on, and continuous.
If a function converges to a nonzero value, its inverse converges to the inverse of this value.
We use the name tendsto.inv₀ as tendsto.inv is already used in multiplicative topological
groups.
If G₀ is a group with zero with topology such that x ↦ x⁻¹ is continuous at all nonzero
points. Then the coercion Mˣ → M is a topological embedding.
Continuity of division #
If G₀ is a group_with_zero with x ↦ x⁻¹ continuous at all nonzero points and (*), then
division (/) is continuous at any point where the denominator is continuous.
Continuity at a point of the result of dividing two functions continuous at that point, where the denominator is nonzero.
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: filter.tendsto_prod_top_iff characterizes this convergence in uniform spaces.
See also filter.prod_top and filter.mem_prod_top.
h x (f x / g x) is continuous under certain conditions, even if the denominator is sometimes
0. See docstring of continuous_at.comp_div_cases.
Left and right multiplication as homeomorphisms #
Left multiplication by a nonzero element in a group_with_zero with continuous multiplication
is a homeomorphism of the underlying type.
Equations
- homeomorph.mul_left₀ c hc = {to_equiv := {to_fun := (equiv.mul_left₀ c hc).to_fun, inv_fun := (equiv.mul_left₀ c hc).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Right multiplication by a nonzero element in a group_with_zero with continuous multiplication
is a homeomorphism of the underlying type.
Equations
- homeomorph.mul_right₀ c hc = {to_equiv := {to_fun := (equiv.mul_right₀ c hc).to_fun, inv_fun := (equiv.mul_right₀ c hc).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}