cnf_empty_satisfiable
theoremverified
The empty CNF formula has no clauses to satisfy, hence is satisfiable under any truth assignment.
Statement
theorem cnf_empty_satisfiable (V : Type*) : CnfSatisfiable (V := V) []
- Verified
- 06 Sep 2026
- Axioms
- none — Lean reports it depends on no axioms
- Built on 1
- CnfSatisfiableA CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains…
Lean source view module on GitHub
/-- The empty CNF formula is vacuously satisfiable. -/ theorem cnf_empty_satisfiable (V : Type*) : CnfSatisfiable (V := V) [] := ⟨fun _ => true, fun _ h => nomatch h⟩