theorem
proved
wrapper
ratio_tau_e_exp_bounds
show as:
view Lean formalization →
formal statement (Lean)
172theorem ratio_tau_e_exp_bounds :
173 (3477 : ℝ) < ratio_tau_e_exp ∧ ratio_tau_e_exp < (3478 : ℝ) := by
proof body
One-line wrapper that applies unfold.
174 unfold ratio_tau_e_exp m_tau_exp m_e_exp; constructor <;> norm_num
175