mathlib documentation

order.order_iso_nat

def rel_embedding.nat_lt {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : → α) :
(∀ (n : ), r (f n) (f (n + 1)))has_lt.lt ↪r r

If f is a strictly r-increasing sequence, then this returns f as an order embedding.

Equations
def rel_embedding.nat_gt {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : → α) :
(∀ (n : ), r (f (n + 1)) (f n))gt ↪r r

If f is a strictly r-decreasing sequence, then this returns f as an order embedding.

Equations
theorem rel_embedding.well_founded_iff_no_descending_seq {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] :