extend_partialOrder

theorem extend_partialOrder : ∀ {α : Type u} (r : α → α → Prop) [inst : IsPartialOrder α r], ∃ s, IsLinearOrder α s ∧ r ≤ s

This theorem states that for any given partial order on a set, it can always be extended to a linear order. The partial order is represented by a relation 'r' on a type 'α'. The theorem guarantees the existence of a relation 's' such that 's' is a linear order on 'α', and every relation in 'r' is also in 's'. In other words, the linear order 's' extends the partial order 'r'.

More concisely: Given any partial order relation on a set, there exists a linear order relation that extends it.