Topological group with zero #
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_group
s. We also use '
in the typeclass name has_continuous_inv'
for the sake of
consistency of notation.
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.
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.
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.