module module

`IndisputableMonolith.CrossDomain.CardinalitySpectrum`

show as: view Lean formalization →

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

generate prose now

declarations in this module (36)

def Dspatial L26
def Dconfig L27
def twoFace L28
def gap45 L29
def eightTick L30
def cubeFaces L31
theorem eightTick_eq L33
theorem gap45_eq L34
theorem cubeFaces_eq L35
theorem three_is_Dspatial L40
theorem four_is_2sq L43
theorem five_is_Dconfig L46
theorem six_is_cubeFaces L49
theorem seven_is_cube_minus_one L52
theorem eight_is_2cube L55
theorem ten_is_2_D L58
theorem twelve_is_D_4 L61
theorem fifteen_is_3_D L64
theorem sixteen_is_2_fourth L67
theorem twentyfive_is_Dsq L70
theorem fortyfive_is_gap L73
theorem sixtyfour_is_2sixth L76
theorem seventy_is_choose_8_4 L79
theorem oneTwentyFive_is_Dcubed L82
theorem twoSixteen_is_six_cubed L85
theorem twoFiftySix_is_power_of_2cube L88
theorem threeSixty_is_tick_gap L91
theorem threeOne25_is_D_fifth L94
theorem eleven_check L99
theorem thirteen_is_fib_7 L103
def rsSpectrum L107
theorem rsSpectrum_length L110
theorem rsSpectrum_pairwise_lt L113
theorem rsSpectrum_bounded L116
structure CardinalitySpectrumCert L119
def cardinalitySpectrumCert L133