Theorems · Definition · combinatorics

IsPredArchimedean.findAtom

{α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : PredOrder α] → [IsPredArchimedean α] → [OrderBot α] → [DecidableEq α] → α → α

The unique atom less than an element in an OrderBot with archimedean predecessor.

Defined in

Mathlib.Order.SuccPred.Tree

Cited by

8 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms

Assumes

PartialOrderPredOrderIsPredArchimedeanOrderBotDecidableEq