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

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

Main statements

• with_gaugeSeminormFamily: the topology of a locally convex space is induced by the family gaugeSeminormFamily.

Todo

• Define the disked hull

Tags

disks, convex, balanced

theorem nhds_basis_abs_convex (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [SMulCommClass ℝ 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace ℝ E] [ContinuousSMul 𝕜 E] : Filter.HasBasis (nhds 0) (fun (s : Set E) => s ∈ nhds 0 ∧ Balanced 𝕜 s ∧ Convex ℝ s) id

theorem nhds_basis_abs_convex_open (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [SMulCommClass ℝ 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace ℝ E] [ContinuousSMul 𝕜 E] [ContinuousSMul ℝ E] [TopologicalAddGroup E] : Filter.HasBasis (nhds 0) (fun (s : Set E) => 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s) id

def AbsConvexOpenSets (𝕜 : Type u_1) (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] : Type u_2

The type of absolutely convex open sets.

Equations

• AbsConvexOpenSets 𝕜 E = { s : Set E // 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s }

noncomputable instance AbsConvexOpenSets.instCoeTC (𝕜 : Type u_1) (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] : CoeTC (AbsConvexOpenSets 𝕜 E) (Set E)

Equations

• AbsConvexOpenSets.instCoeTC 𝕜 E = { coe := Subtype.val }

theorem AbsConvexOpenSets.coe_zero_mem {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : 0 ∈ ↑s

theorem AbsConvexOpenSets.coe_isOpen {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : IsOpen ↑s

theorem AbsConvexOpenSets.coe_nhds {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : ↑s ∈ nhds 0

theorem AbsConvexOpenSets.coe_balanced {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : Balanced 𝕜 ↑s

theorem AbsConvexOpenSets.coe_convex {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : Convex ℝ ↑s

instance AbsConvexOpenSets.instNonempty (𝕜 : Type u_1) (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] : Nonempty (AbsConvexOpenSets 𝕜 E)

Equations

• ⋯ = ⋯

noncomputable def gaugeSeminormFamily (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] : SeminormFamily 𝕜 E (AbsConvexOpenSets 𝕜 E)

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

Equations

• gaugeSeminormFamily 𝕜 E s = gaugeSeminorm ⋯ ⋯ ⋯

theorem gaugeSeminormFamily_ball {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : Seminorm.ball (gaugeSeminormFamily 𝕜 E s) 0 1 = ↑s

theorem with_gaugeSeminormFamily {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [SMulCommClass ℝ 𝕜 E] [LocallyConvexSpace ℝ E] : WithSeminorms (gaugeSeminormFamily 𝕜 E)

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