English
Let q be a seminorm-family generating a uniform structure. For a family f: κ → E → F, the following five statements are equivalent: equicontinuity at 0, equicontinuity, uniform equicontinuity, existence of a continuous bound p for each i with q_i ∘ f k ≤ p, and the i-th seminorm bound's iSup is continuous. This yields a complete characterization of equicontinuity for families of maps into F.
Русский
Пусть q задаёт семинорм-структуру. Для семейства отображений f: κ → E → F равносильно пять утверждений: эконтинуируемость в 0, эконтинуируемость, единообразная эконтинуируемость, существование непрерывной верхней границы p для каждого i с p ≥ q_i ∘ f k, и непрерывность iSup соответствующей композиции. Даёт полное описание эконтинуируемости семей отображений.
LaTeX
$$$WithSeminorms\\ q \\rightarrow\\(TFAE[EquicontinuousAt((\\cdot)\\circ f)0, Equicontinuous((\\cdot)\\circ f), UniformEquicontinuous((\\cdot)\\circ f), ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p, ∀ i, BddAbove (range (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k))]\\)$$
Lean4
theorem cont_normedSpace_to_withSeminorms (E) [SeminormedAddCommGroup E] [NormedSpace 𝕝 E] [TopologicalSpace F]
{q : ι → Seminorm 𝕝₂ F} (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F)
(hf : ∀ i : ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • normSeminorm 𝕝 E) : Continuous f :=
by
rw [← Seminorm.const_isBounded (Fin 1)] at hf
exact continuous_from_bounded (norm_withSeminorms 𝕝 E) hq f hf
