Theorems · Theorem · general topology

Filter.tendsto_const_mul_atBot_of_pos

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

If r is a positive constant, fun x ↦ r * f x tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

Defined in

Mathlib.Order.Filter.AtTopBot.Field

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRing