theorem proved term proof

`rsExists_iff_one`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  40theorem rsExists_iff_one {x : ℝ} (hx : 0 < x) :
  41    RSExists x ↔ x = 1 := by

proof body

Term-mode proof.

  42  unfold RSExists
  43  constructor
  44  · intro h
  45    by_contra hne
  46    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  47  · rintro rfl
  48    exact Jcost_unit0
  49
  50/-- Non-existence costs more than zero. -/

used by (1)

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

costFirstExistenceCert in IndisputableMonolith.Foundation.CostFirstExistence decl_use

depends on (7)

Lean names referenced from this declaration's body.

Jcost_pos_of_ne_one in IndisputableMonolith.Cost decl_use
Jcost_unit0 in IndisputableMonolith.Cost decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Cost.JcostCore decl_use
Jcost_unit0 in IndisputableMonolith.Cost.JcostCore decl_use
RSExists in IndisputableMonolith.Foundation.CostFirstExistence decl_use
RSExists in IndisputableMonolith.Foundation.OntologyPredicates decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Information.LocalCache decl_use