mathlib documentation

order.order_iso_nat

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

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

Equations
source
theorem rel_embedding.well_founded_iff_no_descending_seq {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] :
well_founded r ↔ ¬nonempty (gt ↪r r)