Commit 2024-04-08 10:17 7b7bbd73

View on Github →

chore: remove more bex and ball from lemma names (#11615) Follow-up to #10816. Remaining places containing such lemmas are

  • Option.bex_ne_none and Option.ball_ne_none: defined in Lean core
  • Nat.decidableBallLT and Nat.decidableBallLE: defined in Lean core
  • bef_def is still used in a number of places and could be renamed
  • BAll.imp_{left,right}, BEx.imp_{left,right}, BEx.intro and BEx.elim I only audited the first ~150 lemmas mentioning "ball"; too many lemmas named after Metric.ball/openBall/closedBall.

Estimated changes

deleted theorem Finset.Nonempty.bex
deleted theorem List.not_exists_mem_nil
deleted theorem Set.ball_empty_iff
deleted theorem Set.ball_insert_iff
deleted theorem Set.bex_insert_iff
added theorem Set.exists_mem_insert
added theorem Set.forall_mem_empty
added theorem Set.forall_mem_insert
modified theorem Subgroup.mem_map
modified theorem Submonoid.mem_map
deleted theorem List.bex_cons
deleted theorem List.not_bex_nil
deleted theorem ball_and
deleted theorem ball_cond_comm
deleted theorem ball_congr
deleted theorem ball_mem_comm
deleted theorem ball_or_left
deleted theorem ball_true_iff
deleted theorem bex_congr
deleted theorem bex_imp
deleted theorem bex_of_exists
deleted theorem bex_or
deleted theorem bex_or_left
added theorem exists_mem_of_exists
added theorem exists_mem_or
added theorem exists_mem_or_left
deleted theorem exists_of_bex
added theorem exists_of_exists_mem
added theorem exists₂_imp
added theorem forall_cond_comm
added theorem forall_mem_comm
added theorem forall₂_and
added theorem forall₂_or_left
deleted theorem not_ball
deleted theorem not_ball_of_bex_not
deleted theorem not_bex
added theorem not_exists_mem
added theorem not_forall₂
modified theorem Subring.mem_map