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

rh_from_ontological_dichotomy

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)

 953theorem rh_from_ontological_dichotomy
 954    (h : ∀ sensor : DefectSensor, PhysicallyExists sensor) :
 955    ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False := by

proof body

Term-mode proof.

 956  intro sensor hm
 957  exact hm ((ontological_dichotomy sensor).mpr (h sensor))
 958
 959/-- The converse: RH implies all sensors physically exist (vacuously —
 960charge `0` sensors are T1-bounded). -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.