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

rs_exists_iff_defect_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)

  73theorem rs_exists_iff_defect_zero {x : ℝ} (hx : 0 < x) :
  74    RSExists x ↔ defect x = 0 := by

proof body

Term-mode proof.

  75  constructor
  76  · intro ⟨_, hdef⟩; exact hdef
  77  · intro hdef; exact ⟨hx, hdef⟩
  78
  79/-- The only RSExistent value is 1. -/

depends on (8)

Lean names referenced from this declaration's body.