Theorem not_strictAnti_of_wellFoundedLT

Modification history

2025-01-19 21:48

Mathlib/Order/OrderIsoNat.lean

feat(Order/OrderIsoNat): sequence in well-founded order is not `StrictAnti` (#20851)

Added not_strictAnti_of_wellFoundedLT View on Github →