Commit 2023-04-13 11:50 1f7abb82

View on Github →

feat: port Analysis.LocallyConvex.BalancedCoreHull (#3415) Slightly rewrote the one proof to avoid convert and renamed two lemmas, so that their names fit better with the naming convention.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

added theorem Balanced.balancedHull_subset_of_subset

added theorem Balanced.subset_balancedCore_of_subset

added def balancedCore

added def balancedCoreAux

added theorem balancedCoreAux_balanced

added theorem balancedCoreAux_empty

added theorem balancedCoreAux_maximal

added theorem balancedCoreAux_subset

added theorem balancedCore_balanced

added theorem balancedCore_empty

added theorem balancedCore_eq_interᵢ

added theorem balancedCore_mem_nhds_zero

added theorem balancedCore_nonempty_iff

added theorem balancedCore_subset

added theorem balancedCore_subset_balancedCoreAux

added theorem balancedCore_zero_mem

added theorem balancedHull.balanced

added def balancedHull

added theorem mem_balancedCoreAux_iff

added theorem mem_balancedCore_iff

added theorem mem_balancedHull_iff

added theorem nhds_basis_balanced

added theorem nhds_basis_closed_balanced

added theorem smul_balancedCore_subset

added theorem subset_balancedCore

added theorem subset_balancedHull