mathlib3 documentation


Absolutely convex sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A set is called absolutely convex or disked if it is convex and balanced. The importance of absolutely convex sets comes from the fact that every locally convex topological vector space has a basis consisting of absolutely convex sets.

Main definitions #

Main statements #

Todo #

Tags #

disks, convex, balanced

def abs_convex_open_sets (𝕜 : Type u_1) (E : Type u_2) [topological_space E] [add_comm_monoid E] [has_zero E] [semi_normed_ring 𝕜] [has_smul 𝕜 E] [has_smul E] :
Type u_2

The type of absolutely convex open sets.

Instances for abs_convex_open_sets
@[protected, instance]
@[protected, instance]
noncomputable def gauge_seminorm_family (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [add_comm_group E] [topological_space E] [module 𝕜 E] [module E] [is_scalar_tower 𝕜 E] [has_continuous_smul E] :

The family of seminorms defined by the gauges of absolute convex open sets.

theorem gauge_seminorm_family_ball {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [add_comm_group E] [topological_space E] [module 𝕜 E] [module E] [is_scalar_tower 𝕜 E] [has_continuous_smul E] (s : abs_convex_open_sets 𝕜 E) :

The topology of a locally convex space is induced by the gauge seminorm family.