Theorems · Theorem · functional analysis
Balanced.smul_mem_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] {a : 𝕜} {x : E} [SMulCommClass 𝕝 𝕜 E],
Balanced 𝕝 s → ∀ {b : 𝕝}, a • x ∈ s → ‖b‖ ≤ ‖a‖ → b • x ∈ s- Defined in
- Mathlib.Analysis.LocallyConvex.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Norm.normstatement and proof · cited by 5,413
- IsScalarTowerstatement and proof · cited by 3,896
- SMulCommClassstatement and proof · cited by 1,927
- eq_or_neproof · cited by 1,117
- NormedRingstatement and proof · cited by 924
- norm_nonnegproof · cited by 725
- zero_smulproof · cited by 716
- norm_zeroproof · cited by 366
Cited by1
Results whose statement or proof uses this declaration.
- Balanced.smul_mem_iffproof · cited by 1