Theorems · Theorem · general topology

Filter.eventually_forall_ge_atTop

∀ {α : Type u_3} [inst : Preorder α] {p : α → Prop},
  (∀ᶠ (x : α) in Filter.atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in Filter.atTop, p x

Defined in

Mathlib.Order.Filter.AtTopBot.Finite

Cited by

5 results in Mathlib

Foundations

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

Assumes

Preorder