theorem proved tactic proof

`jfrust_unsat_ge_one`

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

formal statement (Lean)

  38theorem jfrust_unsat_ge_one {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
  39    JFrust f ≥ 1 := by

proof body

Tactic-mode proof.

  40  unfold JFrust
  41  haveI := Classical.propDecidable f.isSAT
  42  have hns : ¬f.isSAT := by
  43    intro ⟨a, ha⟩; exact absurd ha (by simp [h a])
  44  simp [hns]
  45

used by (1)

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

jfrustrationCert in IndisputableMonolith.Complexity.JFrustration decl_use

depends on (2)

Lean names referenced from this declaration's body.

JFrust in IndisputableMonolith.Complexity.JFrustration decl_use
CNFFormula in IndisputableMonolith.Complexity.RSatEncoding decl_use