structure
definition
GraphTheoryDepthCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.GraphTheoryDepthFromRS on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
36def q3ChromaticNumber : ℕ := 2
37theorem q3Chromatic_bipartite : q3ChromaticNumber = 2 := rfl
38
39structure GraphTheoryDepthCert where
40 five_theorems : Fintype.card GraphTheorem = 5
41 euler_q3 : q3EulerChar = 2
42 chromatic_q3 : q3ChromaticNumber = 2
43
44def graphTheoryDepthCert : GraphTheoryDepthCert where
45 five_theorems := graphTheoremCount
46 euler_q3 := q3Euler_eq_2
47 chromatic_q3 := q3Chromatic_bipartite
48
49end IndisputableMonolith.Mathematics.GraphTheoryDepthFromRS