Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-17 07:58 905beb08

View on Github →

fix(topology/metric_space): fix uniform structure on Pi types (#1551)

fix(topology/metric_space): fix uniform structure on pi tpype
cleanup
better construction of metric from emetric
use simp only instead of simp

Estimated changes

Modified src/data/finset.lean

modified theorem finset.sup_le_iff

deleted theorem finset.sup_lt

added theorem finset.sup_lt_iff

Modified src/order/filter/basic.lean

added theorem filter.Inter_mem_sets_of_fintype

added theorem filter.infi_principal_finset

added theorem filter.infi_principal_fintype

Modified src/topology/metric_space/basic.lean

added def emetric_space.to_metric_space_of_dist

Modified src/topology/metric_space/emetric_space.lean