Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-21 11:04 3f915fc5

View on Github →

feat(archive): add the cubing a cube proof (#1343)

  • feat(archive): add the cubing a cube proof
  • rename file
  • add leanpkg configure to travis

Estimated changes

added theorem Ico_lemma
added theorem b_add_w_le_one
added theorem b_le_b
added def bcubes
added theorem bottom_mem_side
added theorem cannot_cube_a_cube
added def correct
added theorem cube.b_lt_xm
added theorem cube.b_mem_bottom
added theorem cube.b_mem_side
added theorem cube.b_mem_to_set
added theorem cube.b_ne_xm
added def cube.bottom
added theorem cube.head_shift_up
added theorem cube.hw'
added def cube.shift_up
added def cube.side
added theorem cube.side_tail
added theorem cube.side_unit_cube
added theorem cube.tail_shift_up
added def cube.to_set
added def cube.unit_cube
added def cube.xm
added structure cube
added theorem exists_mi
added def mi
added theorem mi_mem_bcubes
added theorem mi_minimal
added theorem mi_not_on_boundary'
added theorem mi_not_on_boundary
added theorem mi_strict_minimal
added theorem mi_xm_ne_one
added theorem nonempty_bcubes
added theorem not_correct
added def on_boundary
added theorem side_subset
added theorem smallest_on_boundary
added theorem t_le_t
added theorem tail_sub
added theorem two_le_mk_bcubes
added def valley
added def valley_mi
added theorem valley_unit_cube
added theorem w_lt_w
added theorem w_ne_one
added theorem zero_le_b
added theorem zero_le_of_mem
added theorem zero_le_of_mem_side