Theorems · Theorem · general topology
TopologicalSpace.tendsto_nhds_generateFrom_iff
∀ {α : Type u} {β : Type u_1} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β},
Filter.Tendsto m f (nhds b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f- Defined in
- Mathlib.Topology.Order
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Filterstatement and proof · cited by 8,121
- nhdsstatement · cited by 5,554
- Set.preimagestatement and proof · cited by 4,946
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventuallyproof · cited by 3,134
- TopologicalSpace.generateFromstatement · cited by 62
- TopologicalSpace.nhds_generateFromproof · cited by 15
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.