mathlib documentation

analysis.locally_convex.abs_convex

Absolutely convex sets #

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

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
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
Instances for abs_convex_open_sets
@[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] :
Equations
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) :
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) :
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) :
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
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) :
@[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] :
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
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

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