Theorems · Theorem · real analysis

Filter.Tendsto.rpow

∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ} {x y : ℝ},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → x ≠ 0 ∨ 0 < y → Filter.Tendsto (fun t => f t ^ g t) l (nhds (x ^ y))

Defined in: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Cited by: 4 results in Mathlib
Foundations: Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Filterstatement and proof · cited by 8,121
nhdsstatement and proof · cited by 5,554
Filter.Tendstostatement and proof · cited by 3,814
Filter.Tendsto.compproof · cited by 560
ContinuousAt.tendstoproof · cited by 103
Filter.Tendsto.prodMk_nhdsproof · cited by 46
Real.continuousAt_rpowproof · cited by 3

Cited by4

Results whose statement or proof uses this declaration.

Filter.Tendsto.rpow_constproof · cited by 6
ContinuousAt.rpowproof · cited by 2
Complex.continuousAt_cpow_zero_of_re_posproof · cited by 2
ContinuousWithinAt.rpowproof · cited by 1