Theorems · Theorem · functional analysis

LocallyConvexSpace.convex_basis

∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Semiring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommMonoid E}
  {inst_3 : Module 𝕜 E} {inst_4 : TopologicalSpace E} [self : LocallyConvexSpace 𝕜 E] (x : E),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ Convex 𝕜 s) id

Defined in

Mathlib.Topology.Algebra.Module.LocallyConvex

Cited by

6 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

LocallyConvexSpace