English
Let q be a seminorm-family generating a uniform structure; for a family of maps f, the following statements are equivalent: tight equicontinuity at 0, equicontinuity, uniform equicontinuity, bounded seminorms by a continuous p, and continuity of the supremum seminorms. In particular, knowing continuous seminorms on E characterizes equicontinuity of maps E→F.
Русский
Пусть q задаёт семинорм-структуру; для семейства отображений f указанные ниже условия эквивалентны: эконтинуируемость в точке 0, эконтинуируемость, равномерная эконтинуируемость, ограниченность семинорм всеми f к непрерывной p, и непрерывность iSup семинорм.
LaTeX
$$$hq:\\; WithSeminorms\\ q \\rightarrow\\text{TFAE}[EquicontinuousAt, Equicontinuous, UniformEquicontinuous,\\forall i, \\exists p, Continuous p \\wedge \\forall k, (q_i)\\circ (f k) \\le p,\\forall i, BddAbove(\\text{range}(q_i\\circ f))\\wedge (iSup_k (q_i\\circ f k))]$$$
Lean4
theorem withSeminorms_iff_nhds_eq_iInf [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) :
WithSeminorms p ↔ (𝓝 (0 : E)) = ⨅ i, (𝓝 0).comap (p i) :=
by
rw [← p.filter_eq_iInf]
refine ⟨fun h => ?_, p.withSeminorms_of_nhds⟩
rw [h.topology_eq_withSeminorms]
exact AddGroupFilterBasis.nhds_zero_eq _
