Theorems · Theorem · general topology

Filter.HasBasis.tendsto_left_iff

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β}
  {f : α → β}, la.HasBasis pa sa → (Filter.Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ Set.MapsTo f (sa i) t)

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

9 results in Mathlib

Foundations

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