Theorems · Theorem · general topology

Filter.Tendsto.div_const

∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} {l : Filter α} {x : G₀},
  Filter.Tendsto f l (nhds x) → ∀ (y : G₀), Filter.Tendsto (fun a => f a / y) l (nhds (x / y))

Defined in

Mathlib.Topology.Algebra.GroupWithZero

Cited by

12 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Quot.sound

Assumes

DivInvMonoidTopologicalSpaceSeparatelyContinuousMul