English
Let q be a family of seminorms on a target space F and let f be a family of semilinear maps from E to F indexed by κ. Then the family (↑) ∘ f is uniformly equicontinuous if and only if for every index i there exists a continuous seminorm p on E such that for all k, the i-th seminorm composed with f k is bounded by p; i.e., (q i) ∘ (f k) ≤ p for all k.
Русский
Пусть q — семейство полупнорм на F и пусть f — семейство полиномовых отображений из E в F, индексируемое κ. Тогда совокупность (↑) ∘ f является равномерно экконтинуальной тогда и только тогда, когда для каждого индекса i существует непрерывная полинормa p на E такая, что для всех k выполняется (q i) ∘ f k ≤ p; то есть (q i).comp (f k) ≤ p для всех k.
LaTeX
$$$ UniformEquicontinuous ((\\uparrow) \\circ f) \\iff \\forall i, \\exists p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p $$$
Lean4
theorem _root_.WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm {κ : Type*}
{q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [IsUniformAddGroup F]
(hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) :
UniformEquicontinuous ((↑) ∘ f) ↔ ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p :=
(hq.equicontinuous_TFAE f).out 2 3
