Theorem Finite.wellQuasiOrdered

Modification history

2026-01-09 08:53

Mathlib/Order/WellQuasiOrder.lean

chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)

Modified Finite.wellQuasiOrdered View on Github →

2025-02-13 21:54

Mathlib/Order/WellQuasiOrder.lean

feat(Order/WellQuasiOrder): `WellQuasiOrdered` predicate (#21008) …

Added Finite.wellQuasiOrdered View on Github →