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

source

theorem nhds_basis_abs_convex (𝕜 : Type u_1) (E : Type u_2) [nontrivially_normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [module ℝ E] [smul_comm_class ℝ 𝕜 E] [topological_space E] [locally_convex_space ℝ E] [has_continuous_smul 𝕜 E] :

(nhds 0).has_basis (λ (s : set E), s ∈ nhds 0 ∧ balanced 𝕜 s ∧ convex ℝ s) id

source

theorem nhds_basis_abs_convex_open (𝕜 : Type u_1) (E : Type u_2) [nontrivially_normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [module ℝ E] [smul_comm_class ℝ 𝕜 E] [topological_space E] [locally_convex_space ℝ E] [has_continuous_smul 𝕜 E] [has_continuous_smul ℝ E] [topological_add_group E] :

(nhds 0).has_basis (λ (s : set E), 0 ∈ s ∧ is_open s ∧ balanced 𝕜 s ∧ convex ℝ s) id

source

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.

Equations

abs_convex_open_sets 𝕜 E = {s // 0 ∈ s ∧ is_open s ∧ balanced 𝕜 s ∧ convex ℝ s}

Instances for abs_convex_open_sets

source

@[protected, instance]

def abs_convex_open_sets.has_coe (𝕜 : 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] :

has_coe (abs_convex_open_sets 𝕜 E) (set E)

Equations

abs_convex_open_sets.has_coe 𝕜 E = {coe := subtype.val (λ (s : set E), 0 ∈ s ∧ is_open s ∧ balanced 𝕜 s ∧ convex ℝ s)}

source

theorem abs_convex_open_sets.coe_zero_mem {𝕜 : 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] (s : abs_convex_open_sets 𝕜 E) :

0 ∈ ↑s

source

theorem abs_convex_open_sets.coe_is_open {𝕜 : 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] (s : abs_convex_open_sets 𝕜 E) :

is_open ↑s

source

theorem abs_convex_open_sets.coe_nhds {𝕜 : 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] (s : abs_convex_open_sets 𝕜 E) :

↑s ∈ nhds 0

source

theorem abs_convex_open_sets.coe_balanced {𝕜 : 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] (s : abs_convex_open_sets 𝕜 E) :

balanced 𝕜 ↑s

source

theorem abs_convex_open_sets.coe_convex {𝕜 : 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] (s : abs_convex_open_sets 𝕜 E) :

convex ℝ ↑s

source

@[protected, instance]

def abs_convex_open_sets.nonempty (𝕜 : 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] :

nonempty (abs_convex_open_sets 𝕜 E)

source

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] :

seminorm_family 𝕜 E (abs_convex_open_sets 𝕜 E)

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

Equations

gauge_seminorm_family 𝕜 E = λ (s : abs_convex_open_sets 𝕜 E), gauge_seminorm _ _ _

source

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) :

(gauge_seminorm_family 𝕜 E s).ball 0 1 = ↑s

source

theorem with_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] [topological_add_group E] [has_continuous_smul 𝕜 E] [smul_comm_class ℝ 𝕜 E] [locally_convex_space ℝ E] :

with_seminorms (gauge_seminorm_family 𝕜 E)

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