Theorems · Theorem · general topology
Filter.tendsto_of_seq_tendsto
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated],
(∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l) → Filter.Tendsto f k l- Cited by
- 5 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Filter.IsCountablyGenerated
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- Filter.IsCountablyGeneratedstatement and proof · cited by 220
- Filter.tendsto_iff_seq_tendstoproof · cited by 5
Cited by5
Results whose statement or proof uses this declaration.
- MeasureTheory.AECover.lintegral_tendsto_of_countably_generatedproof · cited by 3
- MeasureTheory.tendsto_of_forall_isClosed_limsup_leproof · cited by 2
- tendsto_integral_mulExpNegMulSq_compproof · cited by 1
- MeasureTheory.tendsto_of_forall_isOpen_le_liminfproof · cited by 1
- MeasureTheory.tendsto_of_forall_isOpen_le_liminf'proof · cited by 1