Theorems · Definition · order theory

RelSeries.append

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

If a₀ -r→ a₁ -r→ ... -r→ aₙ and b₀ -r→ b₁ -r→ ... -r→ bₘ are two strict series such that r aₙ b₀, then there is a chain of length n + m + 1 given by a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ b₀ -r→ b₁ -r→ ... -r→ bₘ.

Defined in

Mathlib.Order.RelSeries

Cited by

11 results in Mathlib

Foundations

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