theorem proved term proof

`possibility_actualization_adjoint`

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

formal statement (Lean)

 392theorem possibility_actualization_adjoint (p : ConfigProp) (c : Config)
 393    (h : possibility_actualization_adjoint_hypothesis p c) :
 394    (◇p) c ↔ p (A c) :=

proof body

Term-mode proof.

 395  h
 396
 397/-! ## Summary -/
 398
 399/-- Status report for Actualization module. -/

used by (1)

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

actualization_status in IndisputableMonolith.Modal.Actualization decl_use

depends on (9)

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Config in IndisputableMonolith.Gravity.ILG decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Status in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint_hypothesis in IndisputableMonolith.Modal.Actualization decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use
ConfigProp in IndisputableMonolith.Modal.Possibility decl_use