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

cost_zero_set_singleton

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)

  33theorem cost_zero_set_singleton :
  34    ∀ x : ℝ, 0 < x → (Jcost x = 0 ↔ x = 1) := by

proof body

Term-mode proof.

  35  intro x hx
  36  constructor
  37  · intro h
  38    by_contra hne
  39    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  40  · rintro rfl; exact Jcost_unit0
  41
  42/-- The cost-zero set in ℝ+ has cardinality 1 (in the sense that any two
  43    members are equal). -/

used by (2)

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

depends on (10)

Lean names referenced from this declaration's body.