Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-11 22:59 0538d2cc

View on Github →

chore(*): reducing imports (#7573)

Estimated changes

Modified src/analysis/special_functions/bernstein.lean

Created src/data/finsupp/antidiagonal.lean

added def finsupp.Iic_finset

added def finsupp.antidiagonal

added theorem finsupp.antidiagonal_support_filter_fst_eq

added theorem finsupp.antidiagonal_support_filter_snd_eq

added theorem finsupp.antidiagonal_zero

added theorem finsupp.coe_Iic_finset

added theorem finsupp.finite_le_nat

added theorem finsupp.finite_lt_nat

added theorem finsupp.mem_Iic_finset

added theorem finsupp.mem_antidiagonal_support

added theorem finsupp.prod_antidiagonal_support_swap

added theorem finsupp.swap_mem_antidiagonal_support

Modified src/data/finsupp/basic.lean

deleted def finsupp.Iic_finset

deleted def finsupp.antidiagonal

deleted theorem finsupp.antidiagonal_support_filter_fst_eq

deleted theorem finsupp.antidiagonal_support_filter_snd_eq

deleted theorem finsupp.antidiagonal_zero

deleted theorem finsupp.coe_Iic_finset

deleted theorem finsupp.finite_le_nat

deleted theorem finsupp.finite_lt_nat

deleted theorem finsupp.mem_Iic_finset

deleted theorem finsupp.mem_antidiagonal_support

deleted theorem finsupp.prod_antidiagonal_support_swap

deleted theorem finsupp.swap_mem_antidiagonal_support

Modified src/data/mv_polynomial/basic.lean

Modified src/order/order_iso_nat.lean

Modified src/topology/algebra/ordered.lean

Modified src/topology/continuous_function/compact.lean

Modified src/topology/continuous_function/weierstrass.lean