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

continuous_space_no_lockIn

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)

 391theorem continuous_space_no_lockIn (x : ℝ) (hx_pos : 0 < x) (hx_exists : defect x = 0) :
 392    ∀ ε > 0, ∃ y : ℝ, y ≠ x ∧ |y - x| < ε := by

proof body

Term-mode proof.

 393  intro ε hε
 394  have hx_eq_one : x = 1 := (defect_zero_iff_one hx_pos).mp hx_exists
 395  subst hx_eq_one
 396  -- Any nearby point exists
 397  use 1 + ε / 2
 398  constructor
 399  · linarith
 400  · simp only [add_sub_cancel_left, abs_of_pos (by linarith : ε / 2 > 0)]
 401    linarith
 402
 403/-! ## Stability in Discrete Spaces -/
 404
 405/-- A discrete configuration space with finite step cost.
 406
 407    In a discrete space, adjacent configurations are separated by a minimum
 408    "gap" in J-cost. This allows configurations to be "trapped" at minima. -/

used by (1)

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

depends on (13)

Lean names referenced from this declaration's body.