Statement of Lemma r.LeBron (lebron_step)

LebronStepStatement β C₀ is the proposition of AVenhance.lebron_step, with the binders (β C₀ : ℝ) turned into arguments.

def AVenhance.Infra.FullTheorem.LebronStepStatement (β C₀ : ℝ) : Prop

The conclusion of Lemma r.LeBron, AVenhance.lebron_step (β C₀ : ℝ).

Equations

• One or more equations did not get rendered due to their size.