module module

`IndisputableMonolith.Cosmology.InterfaceComponentBound`

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

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.LatticeBallEdges module_import
IndisputableMonolith.Cosmology.LatticeBallVolume module_import
IndisputableMonolith.Cosmology.PolarizedBirthDomains module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterface module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount module_import

declarations in this module (37)

def gen L57
def clos L61
theorem clos_equiv L63
def cs L66
def comp L70
theorem eqvGen_le L74
theorem clos_mono_cons L85
def merged L93
theorem merged_equiv L96
theorem gen_cons_le_merged L120
theorem clos_cons_iff L131
def proj L147
theorem card_le_succ_of_merge L153
theorem comp_le_comp_cons L179
theorem comp_congr L193
theorem comp_le_comp_append L207
theorem clos_nil L226
theorem comp_nil L236
theorem comp_eq_one_of_connected L245
theorem mono_components_le_bichromatic_succ L258
theorem clos_root_of_descent L293
theorem connected_of_descent L318
theorem mono_le_interface_of_descent L331
theorem twoCell_connected L344
theorem twoCell_comp_nil L359
theorem twoCell_interface_bound L364
def ball L384
theorem mem_ball_iff L388
abbrev Vtx L397
def height L400
def center L403
def adj L408
def edges L413
theorem mem_edges L416
theorem hzero L422
theorem descent L432
theorem mono_le_interface_succ L463