nonarchimedean_of_emb — Mathlib

English

If a topological group G embeds openly into H and G is nonarchimedean, then H is nonarchimedean.

Русский

Если топологическая группа G открыто встраивается в H и G неархимедова, то H тоже неархимедова.

LaTeX

$$If G is Nonarchimedean and f: G →* H is an open embedding, then NonarchimedeanGroup H.$$

Lean4

/-- If a topological group embeds into a nonarchimedean group, then it is nonarchimedean. -/
@[to_additive]
theorem nonarchimedean_of_emb (f : G →* H) (emb : IsOpenEmbedding f) : NonarchimedeanGroup H :=
  {
    is_nonarchimedean := fun U hU =>
      have h₁ : f ⁻¹' U ∈ 𝓝 (1 : G) := by
        apply emb.continuous.tendsto
        rwa [f.map_one]
      let ⟨V, hV⟩ := is_nonarchimedean (f ⁻¹' U) h₁
      ⟨{ Subgroup.map f V with isOpen' := emb.isOpenMap _ V.isOpen }, Set.image_subset_iff.2 hV⟩ }

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