Theorems · Theorem · functional analysis

LocallyConvexSpace.convex_open_basis_zero

∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [ZeroLEOneClass 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [LocallyConvexSpace 𝕜 E], (nhds 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id

Defined in

Mathlib.Topology.Algebra.Module.LocallyConvex

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldPartialOrderZeroLEOneClassAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousConstSMulLocallyConvexSpace