Mathlib Map

Theorems · Theorem · Lie groups

Filter.tendsto_div_const_iff

∀ {α : Type u} {G : Type u_1} [inst : GroupWithZero G] [inst_1 : TopologicalSpace G] [ContinuousDiv G] {b : G},
  b ≠ 0 →
    ∀ {c : G} {f : α → G} {l : Filter α},
      Filter.Tendsto (fun x => f x / b) l (nhds (c / b)) ↔ Filter.Tendsto f l (nhds c)
Defined in
Mathlib.Topology.Algebra.Group.Basic
Cited by
0 results in Mathlib
Foundations
Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
GroupWithZeroTopologicalSpaceContinuousDiv
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TopologicalSpace · cited by 24529TopologicalSpaceFilter · cited by 8121Filternhds · cited by 5554nhdsFilter.Tendsto · cited by 3814Filter.TendstoGroupWithZero · cited by 691GroupWithZerodiv_one · cited by 629div_oneinv_mul_cancel₀ · cited by 267inv_mul_cancel₀ContinuousDiv · cited by 26ContinuousDivdiv_mul_eq_div_div_swap · cited by 8div_mul_eq_div_div_swapFilter.Tendsto.div_const' · cited by 2Tendsto.div_const'Filter.tendsto_div_const_iffCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.