mathlib documentation

topology.instances.nnreal

@[simp]
theorem nnreal.tendsto_coe {α : Type u_1} {f : filter α} {m : α → ℝ≥0} {x : ℝ≥0} :
filter.tendsto (λ (a : α), (m a)) f (𝓝 x) filter.tendsto m f (𝓝 x)

theorem nnreal.tendsto_coe' {α : Type u_1} {f : filter α} [f.ne_bot] {m : α → ℝ≥0} {x : } :
filter.tendsto (λ (a : α), (m a)) f (𝓝 x) ∃ (hx : 0 x), filter.tendsto m f (𝓝 x, hx⟩)

@[simp]
theorem nnreal.tendsto_coe_at_top {α : Type u_1} {f : filter α} {m : α → ℝ≥0} :

theorem nnreal.tendsto_of_real {α : Type u_1} {f : filter α} {m : α → } {x : } :
filter.tendsto m f (𝓝 x)filter.tendsto (λ (a : α), nnreal.of_real (m a)) f (𝓝 (nnreal.of_real x))

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

theorem nnreal.has_sum_coe {α : Type u_1} {f : α → ℝ≥0} {r : ℝ≥0} :
has_sum (λ (a : α), (f a)) r has_sum f r

theorem nnreal.summable_coe {α : Type u_1} {f : α → ℝ≥0} :
summable (λ (a : α), (f a)) summable f

theorem nnreal.coe_tsum {α : Type u_1} {f : α → ℝ≥0} :
(∑' (a : α), f a) = ∑' (a : α), (f a)

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

theorem nnreal.summable_nat_add (f : ℝ≥0) (hf : summable f) (k : ) :
summable (λ (i : ), f (i + k))

theorem nnreal.sum_add_tsum_nat_add {f : ℝ≥0} (k : ) :
summable f((∑' (i : ), f i) = ∑ (i : ) in finset.range k, f i + ∑' (i : ), f (i + k))

theorem nnreal.infi_real_pos_eq_infi_nnreal_pos {α : Type u_1} [complete_lattice α] {f : → α} :
(⨅ (n : ) (h : 0 < n), f n) = ⨅ (n : ℝ≥0) (h : 0 < n), f n