Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-02 16:36 c0870115

View on Github →

refactor(data/set/finite): make finite argument of set.finite.mem_to_finset explicit (#6508) This way we can use dot notation.

Estimated changes

Modified src/data/finset/preimage.lean

Modified src/data/set/finite.lean

modified theorem set.finite.mem_to_finset

Modified src/linear_algebra/linear_independent.lean

Modified src/measure_theory/integration.lean

Modified src/order/compactly_generated.lean

Modified src/order/filter/cofinite.lean

Modified src/order/order_iso_nat.lean