Theorems · Theorem · general topology

Filter.HasAntitoneBasis.tendsto

∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] {l : Filter α} {s : ι → Set α},
  l.HasAntitoneBasis s → ∀ {φ : ι → α}, (∀ (i : ι), φ i ∈ s i) → Filter.Tendsto φ Filter.atTop l

Defined in

Mathlib.Order.Filter.AtTopBot.Basic

Cited by

2 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Preorder