Theorems · Theorem · functional analysis

SeminormFamily.basisSets_smul_left

∀ {𝕜 : Type u_2} {F : Type u_7} {ι : Type u_9} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : Module 𝕜 F] (p : SeminormFamily 𝕜 F ι) (x : 𝕜),
  ∀ U ∈ p.basisSets, ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedDivisionRingAddCommGroupModule