lemma proved wrapper

`phi_zero`

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)

  33private lemma phi_zero (H : ℝ → ℝ) : Phi H 0 = 0 := by

proof body

One-line wrapper that applies simp.

  34  simp [Phi, intervalIntegral.integral_same]
  35

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

exists_integral_ne_zero in IndisputableMonolith.Cost.AczelProof decl_use
representation_formula in IndisputableMonolith.Cost.AczelProof decl_use
exists_integral_ne_zero in IndisputableMonolith.Cost.AczelTheorem decl_use
phi_zero in IndisputableMonolith.Cost.AczelTheorem decl_use
representation_formula in IndisputableMonolith.Cost.AczelTheorem decl_use

depends on (5)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
Phi in IndisputableMonolith.Cost.AczelProof decl_use
Phi in IndisputableMonolith.Cost.AczelTheorem decl_use
phi_zero in IndisputableMonolith.Cost.AczelTheorem decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use