Theorems · Definition · general topology

Filter.atBot

{α : Type u_3} → [Preorder α] → Filter α

atBot is the filter representing the limit → -∞ on an ordered set. It is generated by the collection of down-sets {b | b ≤ a}. (The preorder need not have a bottom element for this to be well defined, and indeed is trivial when a bottom element x exists, i.e., it coincides with pure x.)

Defined in

Mathlib.Order.Filter.AtTopBot.Defs

Cited by

512 results in Mathlib

Foundations

Depth 15 from the axioms, rests on 87 definitions · uses propext, Quot.sound

Assumes

Preorder