pith. machine review for the scientific record. sign in
structure definition def or abbrev

CostFirstExistenceCert

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)

  91structure CostFirstExistenceCert where
  92  rsExists_iff : ∀ {x : ℝ}, 0 < x → (RSExists x ↔ x = 1)
  93  non_existence_costly :
  94    ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
  95  nothing_diverges :
  96    ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C
  97
  98/-- Cost-first existence certificate. -/

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.