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

RSExists_stable

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)

 468def RSExists_stable (x : ℝ) (config_space : Set ℝ) : Prop :=

proof body

Definition body.

 469  defect x = 0 ∧ ∃ ε > 0, ∀ y ∈ config_space, y ≠ x → |y - x| > ε
 470
 471/-- **Theorem**: RSExists_stable is impossible in connected configuration spaces containing 1.
 472
 473    If config_space is connected and contains 1, then 1 is not isolated,
 474    so RSExists_stable 1 config_space is false. -/

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.