Theorems · Theorem · order theory

setOfPred_minimal_antichain

∀ {α : Type u_1} [inst : PartialOrder α] (P : α → Prop), IsAntichain (fun x1 x2 => x1 ≤ x2) {x | Minimal P x}

Defined in

Mathlib.Order.Antichain

Cited by

5 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

PartialOrder