English
Let q be a family of seminorms on F and f a κ-indexed family of semilinear maps from E to F. Then uniform equicontinuity of (↑) ∘ f is equivalent to: for every i, the set of all values (q i) ∘ (f k) is bounded above, and the iSup over k, namely ⨆ k (q i).comp (f k), is a continuous seminorm on E.
Русский
Пусть q — семейство семинорм на F и f — семейство полиномовых отображений из E в F, индексируемое κ. Тогда равномерно экконтинуальность (↑) ∘ f эквивалентна тому, что для каждого i множество значений (q i) ∘ (f k) ограничено сверху, и ∨_k (q i).comp (f k) является непрерывной нормой на E.
LaTeX
$$$ UniformEquicontinuous ((\\uparrow) \\circ f) \\iff \\forall i,\\ (BddAbove\\ (range\\ (\\lambda k, (q i).comp (f k)))) \\land Continuous (\\big(\\bigvee_{k} (q i).comp (f k)\\big)) $$$
Lean4
theorem _root_.WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup {κ : Type*}
{q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [IsUniformAddGroup F]
(hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) :
UniformEquicontinuous ((↑) ∘ f) ↔
∀ i, BddAbove (range fun k ↦ (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k)) :=
(hq.equicontinuous_TFAE f).out 2 4
