mathlib documentation

theorem nnreal.continuous_of_real  :

theorem nnreal.continuous_coe  :

theorem nnreal.tendsto_coe {α : Type u_1} {f : filter α} {m : α → ℝ≥0} {x : ℝ≥0} :

theorem nnreal.tendsto_of_real {α : Type u_1} {f : filter α} {m : α → ℝ} {x : ℝ} (h : filter.tendsto m f (𝓝 x)) :

theorem nnreal.tendsto.sub {α : Type u_1} {f : filter α} {m n : α → ℝ≥0} {r p : ℝ≥0} (hm : filter.tendsto m f (𝓝 r)) (hn : filter.tendsto n f (𝓝 p)) :

theorem nnreal.continuous_sub  :

theorem nnreal.continuous.sub {α : Type u_1} [topological_space α] {f g : α → ℝ≥0} (hf : continuous f) (hg : continuous g) :

theorem nnreal.has_sum_coe {α : Type u_1} {f : α → ℝ≥0} {r : ℝ≥0} :

theorem nnreal.summable_coe {α : Type u_1} {f : α → ℝ≥0} :

theorem nnreal.coe_tsum {α : Type u_1} {f : α → ℝ≥0} :

theorem nnreal.summable_comp_injective {α : Type u_1} {β : Type u_2} {f : α → ℝ≥0} (hf : summable f) {i : β → α} (hi : function.injective i) :

theorem nnreal.summable_nat_add (f : ℕ → ℝ≥0) (hf : summable f) (k : ℕ) :

theorem nnreal.sum_add_tsum_nat_add {f : ℕ → ℝ≥0} (k : ℕ) (hf : summable f) :