Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-17 13:59 bc72d903

View on Github →

refactor(logic/basic): classical -> root, root -> decidable (#3812) This moves all logic lemmas with decidable instances into the decidable namespace, and moves or adds classical versions of these to the root namespace. This change hits a lot of files, mostly to remove the classical. prefix on explicit references to classical lemmas.

Estimated changes

modified theorem mem_perms_of_list_of_mem
modified theorem and_iff_not_or_not
added theorem by_contra
modified theorem by_contradiction
deleted theorem classical.or_not
added theorem em
modified theorem forall_or_distrib_left
modified theorem forall_or_distrib_right
modified theorem iff_iff_and_or_not_and_not
modified theorem iff_not_comm
modified theorem imp_iff_not_or
modified theorem imp_imp_imp
modified theorem imp_or_distrib'
modified theorem imp_or_distrib
added theorem not.decidable_imp_symm
modified theorem not.imp_symm
deleted theorem not_and_distrib'
modified theorem not_and_distrib
modified theorem not_and_not_right
modified theorem not_ball
modified theorem not_exists_not
modified theorem not_forall
modified theorem not_forall_not
modified theorem not_iff
modified theorem not_iff_comm
modified theorem not_iff_not
modified theorem not_imp
modified theorem not_imp_comm
modified theorem not_imp_not
modified theorem not_not
modified theorem not_or_of_imp
modified theorem of_not_imp
modified theorem of_not_not
modified theorem or_iff_not_and_not
modified theorem or_iff_not_imp_left
modified theorem or_iff_not_imp_right
added theorem or_not
modified theorem peirce