pith. machine review for the scientific record. sign in
lemma proved term proof

stretch_bound

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 167lemma stretch_bound (c : ℝ) : |c| + 1 > 0 := by

proof body

Term-mode proof.

 168  have : 0 ≤ |c| := abs_nonneg _
 169  linarith
 170
 171/-! **Little-o Multiplication**: If f = o(g) and h is bounded, then f·h = o(g·h).
 172    This is a placeholder for the actual asymptotic result. -/
 173
 174end Analysis
 175end Relativity
 176end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.