Commit 2023-05-16 15:19 6a969d40

View on Github →

feat: port Analysis.SpecialFunctions.Log.Basic (#4019) Includes some additional declarations and golfs from #4017.

Estimated changes

added theorem Real.map_exp_nhds
added theorem Real.openEmbedding_exp
added theorem Continuous.log
added theorem ContinuousOn.log
added theorem Filter.Tendsto.log
added theorem Real.continuousAt_log
added theorem Real.continuousOn_log
added theorem Real.continuous_log'
added theorem Real.continuous_log
added theorem Real.cosh_log
added theorem Real.exp_log
added theorem Real.exp_log_eq_abs
added theorem Real.exp_log_of_neg
added theorem Real.le_exp_log
added theorem Real.le_log_iff_exp_le
added theorem Real.log_abs
added theorem Real.log_div
added theorem Real.log_eq_zero
added theorem Real.log_exp
added theorem Real.log_injOn_pos
added theorem Real.log_inv
added theorem Real.log_le_iff_le_exp
added theorem Real.log_le_log
added theorem Real.log_lt_iff_lt_exp
added theorem Real.log_lt_log
added theorem Real.log_lt_log_iff
added theorem Real.log_mul
added theorem Real.log_neg
added theorem Real.log_neg_eq_log
added theorem Real.log_neg_iff
added theorem Real.log_nonneg
added theorem Real.log_nonneg_iff
added theorem Real.log_nonpos
added theorem Real.log_nonpos_iff'
added theorem Real.log_nonpos_iff
added theorem Real.log_of_ne_zero
added theorem Real.log_of_pos
added theorem Real.log_one
added theorem Real.log_pos
added theorem Real.log_pos_iff
added theorem Real.log_pow
added theorem Real.log_prod
added theorem Real.log_sqrt
added theorem Real.log_surjective
added theorem Real.log_zero
added theorem Real.log_zpow
added theorem Real.lt_log_iff_exp_lt
added theorem Real.range_log
added theorem Real.sinh_log
added theorem Real.strictAntiOn_log
added theorem Real.strictMonoOn_log
added theorem Real.surjOn_log'
added theorem Real.surjOn_log
added theorem Real.tendsto_log_atTop