Theorem ChainClosure.succ_fixpoint_iff

Modification history

2025-04-05 18:24

Mathlib/Order/CompleteLattice/Chain.lean

chore(Order/Minimal): don't import `CompleteLattice` (#23592) …

Modified ChainClosure.succ_fixpoint_iff View on Github →

2022-12-29 00:36

Mathlib/Order/Chain.lean

feat: port `Order.Chain` (#1205) …

Added ChainClosure.succ_fixpoint_iff View on Github →