Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 09:36 1ffd04c0

View on Github →

feat(analysis/locally_convex): add balanced hull and core (#12537)

Estimated changes

Created src/analysis/locally_convex/balanced_core_hull.lean

added theorem balanced.hull_subset_of_subset

added theorem balanced.subset_core_of_subset

added def balanced_core

added def balanced_core_aux

added theorem balanced_core_aux_balanced

added theorem balanced_core_aux_empty

added theorem balanced_core_aux_maximal

added theorem balanced_core_aux_mem_iff

added theorem balanced_core_aux_subset

added theorem balanced_core_balanced

added theorem balanced_core_eq_Inter

added theorem balanced_core_mem_iff

added theorem balanced_core_nonempty_iff

added theorem balanced_core_subset

added theorem balanced_core_subset_balanced_core_aux

added theorem balanced_core_zero_mem

added theorem balanced_hull.balanced

added def balanced_hull

added theorem balanced_hull_mem_iff

added theorem smul_balanced_core_subset

added theorem subset_balanced_hull