Theorems · Theorem · general topology

Filter.Tendsto.atTop_mul_const

∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atTop

If a function f tends to infinity along a filter, then f multiplied by a positive constant (on the right) also tends to infinity. For a version working in ℕ or ℤ, use Filter.Tendsto.atTop_mul_const' instead.

Defined in

Mathlib.Order.Filter.AtTopBot.Field

Cited by

12 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemifieldLinearOrderIsStrictOrderedRing