Theorems · Theorem · general topology

Filter.Tendsto.frequently_map

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

Defined in

Mathlib.Order.Filter.Tendsto

Cited by

1 results in Mathlib

Foundations

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