Theorems · Theorem · Lie groups

Filter.TendstoNhdsWithinIoi.mul_const

∀ {α : Type u_2} {𝕜 : Type u_6} [inst : Preorder 𝕜] [inst_1 : Zero 𝕜] [inst_2 : Mul 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [SeparatelyContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b c : 𝕜},
  0 < b →
    ∀ [MulPosStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Ioi c)) →
        Filter.Tendsto (fun a => f a * b) l (nhdsWithin (c * b) (Set.Ioi (c * b)))

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

PreorderZeroMulTopologicalSpaceSeparatelyContinuousMulMulPosStrictMono