theorem proved term proof

`rh_iff_all_physical`

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

formal statement (Lean)

 971theorem rh_iff_all_physical :
 972    (∀ sensor : DefectSensor, sensor.charge ≠ 0 → False) ↔
 973      (∀ sensor : DefectSensor, PhysicallyExists sensor) :=

proof body

Term-mode proof.

 974  ⟨all_physicallyExist_of_rh, rh_from_ontological_dichotomy⟩
 975
 976end UnifiedRH
 977end Unification
 978end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.

DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
all_physicallyExist_of_rh in IndisputableMonolith.Unification.UnifiedRH decl_use
PhysicallyExists in IndisputableMonolith.Unification.UnifiedRH decl_use
rh_from_ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use