@[instance]
Equations
@[instance]
@[instance]
Equations
- nnreal.order_topology = _
- _ = _
- _ = _
theorem
nnreal.tendsto_coe
{α : Type u_1}
{f : filter α}
{m : α → nnreal}
{x : nnreal} :
filter.tendsto (λ (a : α), ↑(m a)) f (nhds ↑x) ↔ filter.tendsto m f (nhds x)
theorem
nnreal.tendsto_of_real
{α : Type u_1}
{f : filter α}
{m : α → ℝ}
{x : ℝ} :
filter.tendsto m f (nhds x) → filter.tendsto (λ (a : α), nnreal.of_real (m a)) f (nhds (nnreal.of_real x))
theorem
nnreal.tendsto.sub
{α : Type u_1}
{f : filter α}
{m n : α → nnreal}
{r p : nnreal} :
filter.tendsto m f (nhds r) → filter.tendsto n f (nhds p) → filter.tendsto (λ (a : α), m a - n a) f (nhds (r - p))
theorem
nnreal.continuous.sub
{α : Type u_1}
[topological_space α]
{f g : α → nnreal} :
continuous f → continuous g → continuous (λ (a : α), f a - g a)
theorem
nnreal.summable_comp_injective
{α : Type u_1}
{β : Type u_2}
{f : α → nnreal}
(hf : summable f)
{i : β → α} :
function.injective i → summable (f ∘ i)