Commit 2023-04-12 19:26 344196ce

View on Github →

feat: port Analysis.LocallyConvex.Basic (#3398)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/Basic.lean

added theorem Absorbent.absorbs

added theorem Absorbent.absorbs_finite

added theorem Absorbent.subset

added theorem Absorbent.zero_mem

added def Absorbent

added theorem Absorbs.add

added theorem Absorbs.inter

added theorem Absorbs.mono

added theorem Absorbs.mono_left

added theorem Absorbs.mono_right

added theorem Absorbs.neg

added theorem Absorbs.sub

added theorem Absorbs.union

added def Absorbs

added theorem Balanced.absorbs_self

added theorem Balanced.add

added theorem Balanced.closure

added theorem Balanced.inter

added theorem Balanced.interior

added theorem Balanced.mem_smul_iff

added theorem Balanced.neg

added theorem Balanced.neg_mem_iff

added theorem Balanced.smul

added theorem Balanced.smul_eq

added theorem Balanced.smul_mono

added theorem Balanced.sub

added theorem Balanced.subset_smul

added theorem Balanced.union

added def Balanced

added theorem Set.Finite.absorbs_unionᵢ

added theorem absorbent_iff_forall_absorbs_singleton

added theorem absorbent_iff_nonneg_lt

added theorem absorbent_nhds_zero

added theorem absorbent_univ

added theorem absorbs_empty

added theorem absorbs_inter

added theorem absorbs_union

added theorem absorbs_unionᵢ_finset

added theorem absorbs_zero_iff

added theorem balanced_convexHull_of_balanced

added theorem balanced_empty

added theorem balanced_iff_neg_mem

added theorem balanced_iff_smul_mem

added theorem balanced_interᵢ

added theorem balanced_interᵢ₂

added theorem balanced_unionᵢ

added theorem balanced_unionᵢ₂

added theorem balanced_univ

added theorem balanced_zero

added theorem balanced_zero_union_interior