Theorems · Theorem · functional analysis

Balanced.smul_mono

∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {s : Set E} [inst_3 : NormedRing 𝕝] [inst_4 : Module 𝕜 𝕝] [NormSMulClass 𝕜 𝕝]
  [inst_6 : SMulWithZero 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {b : 𝕜}, Balanced 𝕝 s → ∀ {a : 𝕝}, ‖a‖ ≤ ‖b‖ → a • s ⊆ b • s

Scalar multiplication (by possibly different types) of a balanced set is monotone.

Defined in

Mathlib.Analysis.LocallyConvex.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedDivisionRingAddCommGroupModuleNormedRingModuleNormSMulClassSMulWithZeroIsScalarTower