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

eps_t_le_one_default

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)

  76lemma eps_t_le_one_default : defaultConfig.eps_t ≤ (1 : ℝ) := by

proof body

Term-mode proof.

  77  norm_num
  78
  79/-- Reference identity under nonzero tick: w_t(τ0, τ0) = 1. -/

depends on (6)

Lean names referenced from this declaration's body.