Theorems · Theorem · general topology
Continuous.tendsto
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → ∀ (x : X), Filter.Tendsto f (nhds x) (nhds (f x))- Defined in
- Mathlib.Topology.Continuous
- Cited by
- 206 results in Mathlib
- Foundations
- Depth 58 from the axioms, rests on 639 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- nhdsstatement · cited by 5,554
- Set.preimageproof · cited by 4,946
- Filter.Tendstostatement · cited by 3,814
- Continuousstatement and proof · cited by 2,592
- IsOpenproof · cited by 2,400
- Set.Subset.rflproof · cited by 255
- IsOpen.preimageproof · cited by 147
- Filter.HasBasis.tendsto_iffproof · cited by 60
- nhds_basis_opensproof · cited by 54
Cited by206
Results whose statement or proof uses this declaration.
- Continuous.continuousAtproof · cited by 297
- continuous_iff_continuousAtproof · cited by 139
- Filter.Tendsto.addproof · cited by 102
- Filter.Tendsto.mulproof · cited by 74
- Filter.Tendsto.subproof · cited by 68
- Filter.Tendsto.const_mulproof · cited by 55
- Continuous.tendsto'proof · cited by 53
- HasSum.mapproof · cited by 32
- Filter.Tendsto.negproof · cited by 30
- Filter.Tendsto.mul_constproof · cited by 23
- Filter.Tendsto.smulproof · cited by 22
- isUniformAddGroup_of_addCommGroupproof · cited by 21
Showing the 200 most cited of 206.