Theorems · Theorem · general topology
tendsto_nhdsWithin_iff
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α},
Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s- Defined in
- Mathlib.Topology.NhdsWithin
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventuallystatement and proof · cited by 3,134
- nhdsWithinstatement and proof · cited by 1,912
- tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_withinproof · cited by 28
- tendsto_nhds_of_tendsto_nhdsWithinproof · cited by 9
- eventually_mem_of_tendsto_nhdsWithinproof · cited by 3
Cited by37
Results whose statement or proof uses this declaration.
- ContDiffWithinAt.isSymmSndFDerivWithinAtproof · cited by 6
- HasFDerivWithinAt.limproof · cited by 4
- mem_tangentConeAt_of_add_smul_memproof · cited by 3
- mem_tangentConeAt_of_frequentlyproof · cited by 3
- IsLocalMaxOn.hasFDerivWithinAt_nonposproof · cited by 3
- tendsto_cobounded_of_meromorphicOrderAt_negproof · cited by 3
- HasFDerivWithinAt.comp_hasFDerivAtproof · cited by 2
- Filter.Tendsto.cfcproof · cited by 2
- Filter.Tendsto.cfc_nnrealproof · cited by 2
- Filter.Tendsto.cfcₙproof · cited by 2
- Filter.Tendsto.cfcₙ_nnrealproof · cited by 2
- blimsup_cthickening_mul_ae_eqproof · cited by 2