# mathlib3documentation

analysis.locally_convex.abs_convex

# 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 #

• gauge_seminorm_family: the seminorm family induced by all open absolutely convex neighborhoods of zero.

## Main statements #

• with_gauge_seminorm_family: the topology of a locally convex space is induced by the family gauge_seminorm_family.

## Todo #

• Define the disked hull

## Tags #

disks, convex, balanced

theorem nhds_basis_abs_convex (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] [ E] [ E] :
(nhds 0).has_basis (λ (s : set E), s nhds 0 s s) id
theorem nhds_basis_abs_convex_open (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] [ E] [ E]  :
(nhds 0).has_basis (λ (s : set E), 0 s s s) id
def abs_convex_open_sets (𝕜 : Type u_1) (E : Type u_2) [has_zero E] [ E] [ E] :
Type u_2

The type of absolutely convex open sets.

Equations
Instances for abs_convex_open_sets
@[protected, instance]
def abs_convex_open_sets.has_coe (𝕜 : Type u_1) (E : Type u_2) [has_zero E] [ E] [ E] :
(set E)
Equations
theorem abs_convex_open_sets.coe_zero_mem {𝕜 : Type u_1} {E : Type u_2} [has_zero E] [ E] [ E] (s : E) :
0 s
theorem abs_convex_open_sets.coe_is_open {𝕜 : Type u_1} {E : Type u_2} [has_zero E] [ E] [ E] (s : E) :
theorem abs_convex_open_sets.coe_nhds {𝕜 : Type u_1} {E : Type u_2} [has_zero E] [ E] [ E] (s : E) :
theorem abs_convex_open_sets.coe_balanced {𝕜 : Type u_1} {E : Type u_2} [has_zero E] [ E] [ E] (s : E) :
s
theorem abs_convex_open_sets.coe_convex {𝕜 : Type u_1} {E : Type u_2} [has_zero E] [ E] [ E] (s : E) :
s
@[protected, instance]
def abs_convex_open_sets.nonempty (𝕜 : Type u_1) (E : Type u_2) [has_zero E] [ E] [ E] :
noncomputable def gauge_seminorm_family (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [ E] [ E] [ E]  :
E)

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

Equations
• = λ (s : , _
theorem gauge_seminorm_family_ball {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] [ E] (s : E) :
s).ball 0 1 = s
theorem with_gauge_seminorm_family {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] [ E] [ E] [ E]  :

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