Theorems · Theorem · general topology
Filter.Tendsto.frequently
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop},
Filter.Tendsto f l₁ l₂ → (∃ᶠ (x : α) in l₁, p (f x)) → ∃ᶠ (y : β) in l₂, p y- Defined in
- Mathlib.Order.Filter.Tendsto
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 15 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.
- Filterstatement and proof · cited by 8,121
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Frequentlystatement and proof · cited by 414
- Filter.Tendsto.eventuallyproof · cited by 174
Cited by12
Results whose statement or proof uses this declaration.
- IsClosed.mem_of_frequently_of_tendstoproof · cited by 5
- mem_closure_of_frequently_of_tendstoproof · cited by 4
- Complex.Gamma_mul_Gamma_add_halfproof · cited by 2
- LiouvilleWith.add_ratproof · cited by 2
- tendsto_nhds_unique_of_frequently_eqproof · cited by 2
- LiouvilleWith.mul_ratproof · cited by 2
- StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticConeproof · cited by 1
- Filter.Tendsto.frequently_mapproof · cited by 1
- Filter.frequently_iff_seq_forallproof · cited by 1
- Nat.frequently_modEqproof · cited by 1
- Convex.asymptoticConeproof · cited by 0
- ApproximatesLinearOn.surjectiveproof · cited by 0