Theorems · Theorem · order theory

WellFounded.min_eq_of_forall_not_lt

∀ {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r] (wf : WellFounded r) {s : Set α} {m : α} (hms : m ∈ s),
  (∀ x ∈ s, ¬r x m) → wf.min s ⋯ = m

The minimal element of a trichotomous well-founded order is unique

Defined in

Mathlib.Order.WellFounded

Cited by

1 results in Mathlib

Foundations

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

Assumes

Std.Trichotomous