Theorems · Definition · order theory

RelSeries.cons

{α : Type u_1} → {r : SetRel α α} → (p : RelSeries r) → (newHead : α) → (newHead, p.head) ∈ r → RelSeries r

Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ and an a such that a₀ -r→ a holds, there is a series of length n+1: a -r→ a₀ -r→ a₁ -r→ ... -r→ aₙ.

Defined in

Mathlib.Order.RelSeries

Cited by

18 results in Mathlib

Foundations

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