CubicPathwidth.T2.All

Source file CubicPathwidth/T2/All.lean of the Lean project (how it is built).

import CubicPathwidth.T2.TargetA
import CubicPathwidth.T2.TargetBC

/-!
# Theorem 2 (maximum degree 4): the three approved targets

`target2a : Target2a`, `target2b : Target2b`, `target2c : Target2c`.
-/

#check (CubicPathwidth.T2.target2a : CubicPathwidth.T2.Target2a)
#check (CubicPathwidth.T2.target2b : CubicPathwidth.T2.Target2b)
#check (CubicPathwidth.T2.target2c : CubicPathwidth.T2.Target2c)
#print axioms CubicPathwidth.T2.target2a
#print axioms CubicPathwidth.T2.target2b
#print axioms CubicPathwidth.T2.target2c
Back to top