map — Mathlib

English

The image of a topologically nilpotent element under a continuous morphism is again topologically nilpotent.

Русский

Образ топологически нильпотентного элемента под непрерывным гомоморфизмом снова топологически нильпотентен.

LaTeX

$$$\text{IsTopologicallyNilpotent}(a) \Rightarrow \text{IsTopologicallyNilpotent}(\varphi(a)).$$$

Lean4

/-- The image of a topologically nilpotent element under a continuous morphism
  is topologically nilpotent -/
theorem map {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S] {φ : F} (hφ : Continuous φ) {a : R}
    (ha : IsTopologicallyNilpotent a) : IsTopologicallyNilpotent (φ a) :=
  by
  unfold IsTopologicallyNilpotent at ha ⊢
  simp_rw [← map_pow]
  exact (map_zero φ ▸ hφ.tendsto 0).comp ha

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