English
If q is a continuous seminorm on a normed space F, then there exists a constant C > 0 such that q(x) ≤ C ||x|| for all x ∈ F.
Русский
Если q — непрерывная семинорм на нормированном пространстве F, то существует постоянная C > 0 такая, что q(x) ≤ C ||x|| для всех x ∈ F.
LaTeX
$$$ \\exists C>0\\;\\forall x:\\, F,\\ q(x) \\le C \\|x\\| $$$
Lean4
/-- Let `F` be a semi-`NormedSpace` over a `NontriviallyNormedField`, and let `q` be a
seminorm on `F`. If `q` is continuous, then it is uniformly controlled by the norm, that is there
is some `C > 0` such that `∀ x, q x ≤ C * ‖x‖`.
The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
norm is then used to rescale any element into an element of norm in `[ε/C, ε[`, thus with a
controlled image by `q`. The control of `q` at the original element follows by rescaling. -/
theorem bound_of_continuous_normedSpace (q : Seminorm 𝕜 F) (hq : Continuous q) :
∃ C, 0 < C ∧ (∀ x : F, q x ≤ C * ‖x‖) :=
by
have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
rcases NormedAddCommGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' <| Iio_mem_nhds one_pos) with ⟨ε, ε_pos, hε⟩
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
have : 0 < ‖c‖ / ε := by positivity
refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
by_cases hx : ‖x‖ = 0
· rw [hx, mul_zero]
exact le_of_eq (map_eq_zero_of_norm_zero q hq hx)
· refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx
refine (le_of_lt <| show q x < _ from hε hlt).trans ?_
rwa [← div_le_iff₀' this, one_div_div]
