Theorem OmegaCompletePartialOrder.Chain.zip_apply

Modification history

2026-04-02 17:24

Mathlib/Order/OmegaCompletePartialOrder.lean

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

Added OmegaCompletePartialOrder.Chain.zip_apply View on Github →