Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-15 22:29 2e90bed8

View on Github →

feat(analysis/complex/exponential): prove that rpow is continuous (#1306)

  • rpow is continuous
  • Update exponential.lean
  • Fix things
  • Fix things
  • Fix things
  • Fix things

Estimated changes

deleted theorem exists_le_mul
added theorem exists_le_mul_self
deleted theorem exists_lt_mul
added theorem exists_lt_mul_self
added theorem real.continuous_at_log
added theorem real.continuous_log'
added theorem real.continuous_log
added theorem real.continuous_rpow
added theorem real.continuous_sqrt
added theorem real.log_lt_log
added theorem real.log_lt_log_iff
added theorem real.log_neg
added theorem real.log_neg_iff
added theorem real.log_nonneg
added theorem real.log_nonpos
added theorem real.log_pos
added theorem real.log_pos_iff
added theorem real.one_lt_rpow
added theorem real.rpow_def_of_neg
added theorem real.rpow_def_of_pos
added theorem real.rpow_lt_one
added theorem real.rpow_lt_rpow
added theorem real.sqrt_eq_rpow
deleted theorem real.continuous_sqrt
added theorem real.exp_lt_one_iff
added theorem real.one_lt_exp_iff