Theorems · Theorem · functional analysis

Filter.HasBasis.isVonNBounded_iff

∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {q : ι → Prop} {s : ι → Set E} {A : Set E},
  (nhds 0).HasBasis q s → (Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A)

Defined in

Mathlib.Analysis.LocallyConvex.Bounded

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedRingSMulZeroTopologicalSpace