Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-20 22:14 e2a562a8

View on Github →

refactor(analysis/topology): simplify is_topological_basis_of_open_of_nhds

Estimated changes

Modified algebra/big_operators.lean

modified theorem finset.prod_attach

modified theorem finset.prod_bij

modified theorem finset.prod_bij_ne_one

Modified analysis/measure_theory/borel_space.lean

Modified analysis/topology/topological_space.lean

Modified data/encodable.lean

Modified data/fintype.lean

added def set_fintype