Theorem wellQuasiOrdered_iff_exists_monotone_subseq

Modification history

2025-02-13 21:54
Mathlib/Order/WellQuasiOrder.lean
feat(Order/WellQuasiOrder): `WellQuasiOrdered` predicate (#21008) …
Added wellQuasiOrdered_iff_exists_monotone_subseqView on Github →