def
definition
powerSetQ3
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.SetTheoryFromRS on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
28theorem fundamentalZFCount : Fintype.card FundamentalZFAxiom = 5 := by decide
29
30/-- Power set of Q₃ = 2^8 = 256. -/
31def powerSetQ3 : ℕ := 2 ^ 8
32theorem powerSetQ3_eq_256 : powerSetQ3 = 256 := by decide
33
34/-- 256 = 2^(2^D). -/
35theorem powerSetQ3_2_2D : powerSetQ3 = 2 ^ (2 ^ 3) := by decide
36
37structure SetTheoryCert where
38 five_axioms : Fintype.card FundamentalZFAxiom = 5
39 power_set_256 : powerSetQ3 = 256
40 structure_match : powerSetQ3 = 2 ^ (2 ^ 3)
41
42def setTheoryCert : SetTheoryCert where
43 five_axioms := fundamentalZFCount
44 power_set_256 := powerSetQ3_eq_256
45 structure_match := powerSetQ3_2_2D
46
47end IndisputableMonolith.Mathematics.SetTheoryFromRS