Theorems · Theorem · order theory

Set.partiallyWellOrderedOn_iff_finite_antichains

∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [Std.Refl r] [Std.Symm r],
  s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite

Defined in

Mathlib.Order.WellFoundedSet

Cited by

0 results in Mathlib

Foundations

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

Assumes

Std.ReflStd.Symm