Commit 2024-09-12 09:57 2f55b8c9

View on Github →

chore: deprecate 14 Init.Logic lemmas (#16721) Deprecate

  • (and,or,iff)_(true,false)_iff and (true,false)_(and_or_iff)_iff for the lemmas without _iff, which are in core
  • iff_self_iff for iff_self in core
  • not_or_of_not for not_or_intro in core The vast majority of their uses are as simp/rw lemmas, for which the core versions work equally well.

Estimated changes

modified theorem MonoidHom.ker_fst
modified theorem MonoidHom.ker_snd
modified theorem MonoidHom.mker_fst
modified theorem MonoidHom.mker_snd
modified theorem Set.empty_sigma
modified theorem Set.sigma_empty
modified theorem Set.univ_sigma_univ
deleted theorem not_or_of_not
modified theorem Finset.left_mem_Icc
modified theorem Finset.left_mem_Ico
modified theorem Finset.right_mem_Icc
modified theorem Finset.right_mem_Ioc