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.
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.
Instances
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.
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.
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.
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.
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: 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 ContinuousAt.comp_div_cases.
Left and right multiplication as homeomorphisms #
Left multiplication by a nonzero element in a GroupWithZero with continuous multiplication
is a homeomorphism of the underlying type.
Equations
- Homeomorph.mulLeft₀ c hc = { toEquiv := Equiv.mulLeft₀ c hc, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Right multiplication by a nonzero element in a GroupWithZero with continuous multiplication
is a homeomorphism of the underlying type.
Equations
- Homeomorph.mulRight₀ c hc = { toEquiv := Equiv.mulRight₀ c hc, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
If a group with zero has continuous multiplication and fun x ↦ x⁻¹ is continuous at one,
then it is continuous at any unit.