Theorem RelEmbedding.not_wellFounded

Modification history

2025-08-15 22:00

Mathlib/Order/OrderIsoNat.lean

feat(Order/WellFounded): Acc and infinite descending chain (#28120)

Added RelEmbedding.not_wellFounded View on Github →