Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-29 18:27 07726e21

View on Github →

chore(analysis/locally_convex/balanced_core_hull): Golf (#14987) Golf and improve lemmas based on the naming convention:

  • balanced_mem → balanced_iff_smul_mem
  • zero_singleton_balanced → balanced_zero
  • balanced_core_emptyset → balanced_core_empty
  • balanced_core_mem_iff → mem_balanced_core_iff
  • balanced_hull_mem_iff → mem_balanced_hull_iff
  • balanced_core_is_closed → is_closed.balanced_core

Estimated changes

modified theorem balanced_core_aux_balanced
modified theorem balanced_core_aux_maximal
deleted theorem balanced_core_aux_mem_iff
added theorem balanced_core_empty
deleted theorem balanced_core_emptyset
modified theorem balanced_core_eq_Inter
deleted theorem balanced_core_is_closed
deleted theorem balanced_core_mem_iff
modified theorem balanced_core_mem_nhds_zero
modified theorem balanced_core_nonempty_iff
modified theorem balanced_core_subset
modified theorem balanced_core_zero_mem
deleted theorem balanced_hull_mem_iff
added theorem mem_balanced_core_iff
added theorem mem_balanced_hull_iff
modified theorem subset_balanced_core
added theorem balanced_iff_smul_mem
deleted theorem balanced_mem
added theorem balanced_zero
deleted theorem zero_singleton_balanced