Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-12 01:16 113568c9

View on Github →

refactor(archive/100-theorems-list/02_cubing_a_cube): review API (#16898)

  • reuse lemmas about set.pi;
  • fix some def/lemma;
  • use nontrivial and set.nontrivial instead of 2 ≤ cardinal.mk ι;
  • redefine correct as a structure.

Estimated changes

deleted theorem b_add_w_le_one
added theorem correct.b_add_w_le_one
added theorem correct.nontrivial_fin
added theorem correct.side_subset
added theorem correct.w_ne_one
added theorem correct.zero_le_b
added theorem correct.zero_le_of_mem
added structure correct
deleted def correct
added theorem cube.side_nonempty
added theorem cube.to_set_disjoint
added theorem cube.to_set_subset
deleted def cube.to_set_subset
added theorem cube.univ_pi_side
modified theorem exists_mi
added theorem nontrivial_bcubes
deleted theorem side_subset
deleted theorem to_set_subset_unit_cube
deleted theorem two_le_mk_bcubes
added theorem valley_mi
deleted def valley_mi
modified theorem valley_unit_cube
deleted theorem w_ne_one
deleted theorem zero_le_b
deleted theorem zero_le_of_mem
deleted theorem zero_le_of_mem_side