Mathlib v3 is deprecated. Go to Mathlib v4

Theorem disjoint_assoc

Modification history

2022-11-27 23:52

src/order/bounded_order.lean

chore(order/bounded_order): split (#17730) …

Modified disjoint_assoc View on Github →

2022-05-24 10:24

src/order/bounded_order.lean

chore(order/bounded_order): Golf `disjoint` API (#14194) …

Modified disjoint_assoc View on Github →

2022-01-26 23:35

src/order/bounded_order.lean

feat(order/filter): +1 version of `mem_inf_principal` (#11674)

Added disjoint_assoc View on Github →