mathlib
07726e21 - chore(analysis/locally_convex/balanced_core_hull): Golf (#14987)

Commit
3 years ago
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`
Author
Parents
Loading