Theorems · Theorem · general topology
Filter.tendsto_pure_pure
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), Filter.Tendsto f (pure a) (pure (f a))- Defined in
- Mathlib.Order.Filter.Tendsto
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement · cited by 8,121
- Filter.Tendstostatement · cited by 3,814
- Filter.tendsto_pureproof · cited by 23
Cited by25
Results whose statement or proof uses this declaration.
- HasFDerivAt.compproof · cited by 50
- HasDerivAt.compproof · cited by 43
- HasDerivAt.comp_hasFDerivWithinAtproof · cited by 22
- HasDerivAt.comp_hasFDerivAtproof · cited by 20
- HasDerivAt.scompproof · cited by 11
- HasFDerivWithinAt.compproof · cited by 11
- tendsto_pure_nhdsproof · cited by 7
- HasDerivWithinAt.scompproof · cited by 7
- HasFDerivWithinAt.comp_hasFDerivAtproof · cited by 2
- HasFDerivWithinAt.iterateproof · cited by 2
- HasDerivWithinAt.scomp_hasDerivAtproof · cited by 2
- HasDerivWithinAt.comp_hasDerivAtproof · cited by 1