Theorems · Theorem · functional analysis
rescale_to_shell_semi_normed
∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
{c : 𝕜},
1 < ‖c‖ →
∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, ‖x‖ ≠ 0 → ∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖If there is a scalar c with ‖c‖>1, then any element with nonzero norm can be
moved by scalar multiplication to any shell of width ‖c‖. Also recap information on the norm of
the rescaling element that shows up in applications.
- Defined in
- Mathlib.Analysis.Seminorm
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedSpacestatement and proof · cited by 12,499
- Norm.normstatement and proof · cited by 5,413
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- NormedFieldstatement and proof · cited by 1,084
- normSeminormproof · cited by 32
- Seminorm.rescale_to_shellproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- rescale_to_shellproof · cited by 4
- egauge_ball_le_of_one_lt_normproof · cited by 4
- MultilinearMap.bound_of_shell_of_norm_map_coord_zeroproof · cited by 3