Theorems · Theorem · order theory

transGen_of_pred_of_gt

∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → m < n → Relation.TransGen r n m

For m < n, (n, m) is in the transitive closure of a relation ~ for n ≠ m if i ~ pred i for all i between n and m.

Defined in

Mathlib.Order.SuccPred.Relation

Cited by

0 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderPredOrderIsPredArchimedean