Theorems · Theorem · functional analysis

nhds_hasBasis_absConvex

∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E],
  (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ AbsConvex 𝕜 s) id

Defined in

Mathlib.Analysis.LocallyConvex.AbsConvex

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldPartialOrderAddCommGroupModuleTopologicalSpaceLocallyConvexSpaceContinuousSMul