Theorems · Theorem · real analysis
Real.log_injOn_pos
Set.InjOn Real.log (Set.Ioi 0)
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Set.Ioistatement · cited by 1,463
- Real.logstatement · cited by 939
- Set.InjOnstatement · cited by 543
- StrictMonoOn.injOnproof · cited by 22
- Real.strictMonoOn_logproof · cited by 13
Cited by7
Results whose statement or proof uses this declaration.
- Real.log_lt_sub_one_of_posproof · cited by 4
- Real.geom_mean_eq_arith_mean_weighted_iff_of_pos'proof · cited by 4
- Real.eq_one_of_pos_of_log_eq_zeroproof · cited by 2
- Real.rpow_logb_eq_absproof · cited by 2
- Real.eq_Gamma_of_log_convexproof · cited by 1
- sum_div_pow_sq_le_div_sqproof · cited by 1
- Real.mul_log_eq_log_iffproof · cited by 0