theorem
proved
wrapper
codata_very_small
show as:
view Lean formalization →
formal statement (Lean)
195theorem codata_very_small : alphaG_codata < 1e-40 := by
proof body
One-line wrapper that applies unfold.
196 unfold alphaG_codata; norm_num
197