Theorems · Theorem · general topology

Filter.tendsto_iff_eventually

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)

Defined in

Mathlib.Order.Filter.Tendsto

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound