Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 03:53 31cd6dd2

View on Github →

chore(order/bounded_lattice): use ⦃⦄ in disjoint.symm (#3893)

Estimated changes

Modified src/data/set/disjointed.lean

Modified src/order/bounded_lattice.lean

modified theorem disjoint.symm