Structure OmegaCompletePartialOrder.Chain

Modification history

2026-04-02 17:24

Mathlib/Order/OmegaCompletePartialOrder.lean

refactor(Order/OmegaCompletePartialOrder): make `Chain` a `structure` (#37258) …

Added OmegaCompletePartialOrder.Chain View on Github →