Theorems · Theorem · general topology

Filter.eventuallyConst_atTop

∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : SemilatticeSup α] [Nonempty α],
  Filter.EventuallyConst f Filter.atTop ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i

Defined in

Mathlib.Order.Filter.EventuallyConst

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemilatticeSupNonempty