Theorems · Theorem · functional analysis

Asymptotics.isLittleOTVS_one

∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} {f : α → E} [ContinuousSMul 𝕜 E],
  f =o[𝕜; l] 1 ↔ Filter.Tendsto f l (nhds 0)

Defined in: Mathlib.Analysis.Asymptotics.TVS
Cited by: 4 results in Mathlib
Foundations: Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField AddCommGroup TopologicalSpace Module ContinuousSMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites64

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

Setproof · cited by 53,352
Realproof · cited by 25,697
TopologicalSpacestatement and proof · cited by 24,529
Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
ENNRealproof · cited by 9,879
NontriviallyNormedFieldstatement and proof · cited by 8,742
Filterstatement and proof · cited by 8,121
nhdsstatement and proof · cited by 5,554
Norm.normproof · cited by 5,413
Set.preimageproof · cited by 4,946
NNRealproof · cited by 4,310

Cited by4

Results whose statement or proof uses this declaration.

HasFDerivWithinAt.limproof · cited by 4
HasFDerivAtFilter.tendsto_nhdsproof · cited by 4
Asymptotics.IsLittleOTVS.tendsto_inv_smulproof · cited by 1
Asymptotics.isLittleOTVS_iff_tendsto_inv_smulproof · cited by 0