congr_equiv — Mathlib

English

If a family p is transformed by an equivalence e on the index set, the new family p ∘ e generates the same topology as p.

Русский

Если семейство p преобразуется с помощью эквивалентности e на множестве индексов, то новое семейство p ∘ e порождает ту же топологию, что и p.

LaTeX

$$$ WithSeminorms p \\to \\Forall (e: ι' ≃ ι), WithSeminorms (p \\circ e) $$$

Lean4

protected theorem congr_equiv {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) (e : ι' ≃ ι) :
    WithSeminorms (p ∘ e) := by refine hp.congr ?_ ?_ <;> intro i <;> [use {e i}, 1; use {e.symm i}, 1] <;> simp

Похожие утверждения