Theorems · Theorem · Lie groups

Filter.TendstoNhdsWithinIoi.const_mul

∀ {α : 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 →
    ∀ [PosMulStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Ioi c)) →
        Filter.Tendsto (fun a => b * f a) l (nhdsWithin (b * c) (Set.Ioi (b * c)))

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderZeroMulTopologicalSpaceSeparatelyContinuousMulPosMulStrictMono