theorem proved term proof

`modal_duality`

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

formal statement (Lean)

 331theorem modal_duality (p : ConfigProp) (c : Config) :
 332    (□p) c ↔ ¬(◇(fun x => ¬p x)) c := by

proof body

Term-mode proof.

 333  constructor
 334  · intro h ⟨y, hy, hny⟩
 335    exact hny (h y hy)
 336  · intro h y hy
 337    by_contra hc
 338    exact h ⟨y, hy, hc⟩
 339
 340/-- Distribution: □(p → q) → (□p → □q) -/

depends on (3)

Lean names referenced from this declaration's body.

Config in IndisputableMonolith.Gravity.ILG decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use
ConfigProp in IndisputableMonolith.Modal.Possibility decl_use