Theorems · Theorem · order theory

transGen_of_succ_of_refl

∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α}
  [Std.Refl r],
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → Relation.TransGen r n m

(n, m) is in the transitive closure of a reflexive relation ~ if i ~ succ i and succ i ~ i for all i between n and m.

Defined in

Mathlib.Order.SuccPred.Relation

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderSuccOrderIsSuccArchimedeanStd.Refl