theorem proved term proof

`zero_pos_dist`

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

formal statement (Lean)

  99theorem zero_pos_dist : ¬Indistinguishable signRecognizer 0 1 := by

proof body

Term-mode proof.

 100  simp [Indistinguishable, signRecognizer, signOf]
 101
 102/-! ## Example 3: Magnitude Recognizer on ℤ -/
 103
 104/-- The magnitude recognizer: n ↦ |n| -/

depends on (3)

Lean names referenced from this declaration's body.

signOf in IndisputableMonolith.RecogGeom.Examples decl_use
signRecognizer in IndisputableMonolith.RecogGeom.Examples decl_use
Indistinguishable in IndisputableMonolith.RecogGeom.Indistinguishable decl_use