Theorems · Theorem · general topology
Filter.Tendsto.eventually_mem
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β},
Filter.Tendsto f l₁ l₂ → s ∈ l₂ → ∀ᶠ (x : α) in l₁, f x ∈ s- Defined in
- Mathlib.Order.Filter.Tendsto
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventuallystatement · cited by 3,134
Cited by20
Results whose statement or proof uses this declaration.
- Filter.tendsto_of_subseq_tendstoproof · cited by 3
- Hyperreal.lt_of_tendsto_atBotproof · cited by 3
- Hyperreal.lt_of_tendsto_atTopproof · cited by 3
- ConvexOn.isBoundedUnder_absproof · cited by 2
- MvPolynomial.toMvPowerSeries_uniformContinuousproof · cited by 2
- Convex.interior_closure_eq_interior_of_nonempty_interiorproof · cited by 1
- LinearMap.continuousAt_zero_of_locally_boundedproof · cited by 1
- ContinuousSMul.topology_eq_of_nhds_inf_principal_eqproof · cited by 1
- Asymptotics.Filter.Tendsto.isBigOTVS_oneproof · cited by 1
- MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeffproof · cited by 1
- IsVisible.eq_of_mem_interiorproof · cited by 1
- IsTopologicallyNilpotent.exists_pow_mem_of_mem_nhdsproof · cited by 1