English
If two seminorm families p and q on the same space generate the same topology, provided each p i is bounded by some C times a finite supremum of q and vice versa (in the sense of IsBounded against the identity map), then q also generates the same topology as p.
Русский
Если два семейства семинорм p и q на одном пространстве порождают одну и ту же топологию, и при этом каждое p i ограничено некоторым C на Finset.sup q и наоборот, в смысле ограниченности по тождественному отображению, то q порождает ту же топологию, что и p.
LaTeX
$$$ WithSeminorms p \\to Seminorm.IsBounded p q LinearMap.id \\to Seminorm.IsBounded q p LinearMap.id \\to WithSeminorms q $$$
Lean4
/-- Two families of seminorms `p` and `q` on the same space generate the same topology
if each `p i` is bounded by some `C • Finset.sup s q` and vice-versa.
We formulate these boundedness assumptions as `Seminorm.IsBounded q p LinearMap.id` (and
vice-versa) to reuse the API. Furthermore, we don't actually state it as an equality of topologies
but as a way to deduce `WithSeminorms q` from `WithSeminorms p`, since this should be more
useful in practice. -/
protected theorem congr {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'} [t : TopologicalSpace E]
(hp : WithSeminorms p) (hpq : Seminorm.IsBounded p q LinearMap.id) (hqp : Seminorm.IsBounded q p LinearMap.id) :
WithSeminorms q := by
constructor
rw [hp.topology_eq_withSeminorms]
clear hp t
refine le_antisymm ?_ ?_ <;> rw [← continuous_id_iff_le] <;>
refine continuous_from_bounded (.mk (topology := _) rfl) (.mk (topology := _) rfl) LinearMap.id (by assumption)
