Absolutely convex open sets

A set s in a commutative monoid E equipped with a topology is said to be an absolutely convex open set if it is absolutely convex and open. When E is a topological additive group, the topology coincides with the topology induced by the family of seminorms arising as gauges of absolutely convex open neighborhoods of zero.

Main definitions

• AbsConvexOpenSets: sets which are absolutely convex and open
• 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.

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 ∧ AbsConvex 𝕜 s }

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

Equations

• AbsConvexOpenSets.instCoeOut 𝕜 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)

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) : (gaugeSeminormFamily 𝕜 E s).ball 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] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [SMulCommClass ℝ 𝕜 E] [LocallyConvexSpace ℝ E] : WithSeminorms (gaugeSeminormFamily 𝕜 E)

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