Theorems · Theorem · order theory

IsChain.total

∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {x y : α} [Std.Refl r], IsChain r s → x ∈ s → y ∈ s → r x y ∨ r y x

Defined in

Mathlib.Order.Preorder.Chain

Cited by

12 results in Mathlib

Foundations

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

Assumes

Std.Refl