Theorems · Theorem · general topology

Filter.Tendsto.eventually_forall_le_atBot

∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} {p : β → Prop} {f : α → β},
  Filter.Tendsto f l Filter.atBot → (∀ᶠ (x : β) in Filter.atBot, p x) → ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Defined in

Mathlib.Order.Filter.AtTopBot.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

Preorder