Theorems · Theorem · general topology

Filter.tendsto_mul_const_atTop_iff_neg

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

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x * r tends to infinity if and only if r < 0.

Defined in

Mathlib.Order.Filter.AtTopBot.Field

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingFilter.NeBot