Topology on ℝ≥0
#
The natural topology on ℝ≥0
(the one induced from ℝ
), and a basic API.
Main definitions #
Instances for the following typeclasses are defined:
topological_space ℝ≥0
topological_semiring ℝ≥0
second_countable_topology ℝ≥0
order_topology ℝ≥0
has_continuous_sub ℝ≥0
has_continuous_inv₀ ℝ≥0
(continuity ofx⁻¹
away from0
)has_continuous_smul ℝ≥0 ℝ
Everything is inherited from the corresponding structures on the reals.
Main statements #
Various mathematically trivial lemmas are proved about the compatibility
of limits and sums in ℝ≥0
and ℝ
. For example
tendsto_coe {f : filter α} {m : α → ℝ≥0} {x : ℝ≥0} : tendsto (λa, (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ tendsto m f (𝓝 x)
says that the limit of a filter along a map to ℝ≥0
is the same in ℝ
and ℝ≥0
, and
coe_tsum {f : α → ℝ≥0} : ((∑'a, f a) : ℝ) = (∑'a, (f a : ℝ))
says that says that a sum of elements in ℝ≥0
is the same in ℝ
and ℝ≥0
.
Similarly, some mathematically trivial lemmas about infinite sums are proved, a few of which rely on the fact that subtraction is continuous.
Equations
Embedding of ℝ≥0
to ℝ
as a bundled continuous map.
Equations
The sum over the complement of a finset tends to 0
when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero.