Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-01 15:07 431551a8

View on Github →

refactor(topology/algebra): use the dot notation in continuous_mul and friends (#1758)

  • continuous_add
  • fixes
  • more fixes
  • fix
  • tendsto_add
  • fix tendsto
  • last fix

Estimated changes

added theorem filter.tendsto.mul_mul
deleted theorem filter.tendsto_mul_mul
added theorem continuous.inv
added theorem continuous.sub
deleted theorem continuous_inv'
modified theorem continuous_inv
deleted theorem continuous_sub'
modified theorem continuous_sub
added theorem tendsto.inv
added theorem tendsto.sub
deleted theorem tendsto_inv
deleted theorem tendsto_sub
added theorem continuous.mul
deleted theorem continuous_mul'
modified theorem continuous_mul
added theorem tendsto.mul
deleted theorem tendsto_mul'
modified theorem tendsto_mul
added theorem continuous.max
added theorem continuous.min
deleted theorem continuous_max
deleted theorem continuous_min
added theorem tendsto.max
added theorem tendsto.min
deleted theorem tendsto_max
deleted theorem tendsto_min
added theorem uniform_continuous.add
added theorem uniform_continuous.neg
added theorem uniform_continuous.sub
deleted theorem uniform_continuous_add'
modified theorem uniform_continuous_add
deleted theorem uniform_continuous_neg'
modified theorem uniform_continuous_neg
deleted theorem uniform_continuous_sub'
modified theorem uniform_continuous_sub
added theorem complex.continuous.inv
deleted theorem complex.continuous_inv'
modified theorem complex.continuous_inv
added theorem nnreal.continuous.sub
deleted theorem nnreal.continuous_sub'
modified theorem nnreal.continuous_sub
added theorem nnreal.tendsto.sub
deleted theorem nnreal.tendsto_sub
added theorem real.continuous.inv
deleted theorem real.continuous_inv'
modified theorem real.continuous_inv