Theorems · Theorem · functional analysis

nhds_hasBasis_absConvex_open

∀ (𝕜 : 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]
  [IsTopologicalAddGroup E] [ZeroLEOneClass 𝕜], (nhds 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s) id

Defined in

Mathlib.Analysis.LocallyConvex.AbsConvex

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldPartialOrderAddCommGroupModuleTopologicalSpaceLocallyConvexSpaceContinuousSMulIsTopologicalAddGroupZeroLEOneClass