Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 23:35 a1e1ffd1

View on Github →

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

Estimated changes

Modified src/order/bounded_order.lean

added theorem disjoint_assoc

Modified src/order/filter/basic.lean

added theorem filter.mem_inf_principal'