Meets in bounded pred-archimedean orders

[UPSTREAM] candidate for Mathlib/Order/SuccPred/Tree.lean: in a partial order with a bottom, predecessors, and archimedean descent — the unbundled data of a rooted tree — binary meets exist: a ⊓ b is the first pred-iterate of a that lies below b. RootedTree currently asks for SemilatticeInf as a field; on orders with decidable ≤ it is derivable.

theorem IsPredArchimedean.exists_pred_iterate_le {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] (a b : α) : ∃ (i : ℕ), Order.pred^[i] a ≤ b

Some pred-iterate of a lies below b: descend all the way to ⊥.

@[reducible]

def IsPredArchimedean.semilatticeInf {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : SemilatticeInf α

Binary meets from archimedean descent: a ⊓ b is the first pred-iterate of a below b. Not an instance: a type may already carry a SemilatticeInf that this construction need not match definitionally.

Equations

• IsPredArchimedean.semilatticeInf = { toPartialOrder := inst✝⁴, inf := fun (a b : α) => Order.pred^[Nat.find ⋯] a, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }