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

proxyPhysicalizationBridge_iff_charge_zero

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)

 105theorem proxyPhysicalizationBridge_iff_charge_zero (sensor : DefectSensor) :
 106    ProxyPhysicalizationBridge sensor ↔ sensor.charge = 0 :=

proof body

Term-mode proof.

 107  (proxyPhysicalizationBridge_iff_physicallyExists sensor).trans
 108    (charge_zero_iff_physicallyExists sensor).symm
 109
 110/-- The bridge holds unconditionally for charge-zero sensors. -/

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.