map — Mathlib

English

If φ is a continuous ring homomorphism and a has evaluation, then the evaluation map commutes with φ, i.e., composing φ with evaluation yields evaluation after mapping.

Русский

Если φ непрерывное гомоморфизм кольца и a имеет оценку, то отображение оценки коммутирует с φ.

LaTeX

$$$\\text{Continuous } φ \\;\\Rightarrow\\; \\text{HasEval } a \\Rightarrow (\\text{eval}_{φ}(a)) = φ \\circ \\text{eval}_{a}$$$

Lean4

/-- [Bourbaki, *Algebra*, chap. 4, §4, n°3, Prop. 4 (i) (a & b)][bourbaki1981]. -/
theorem map (hφ : Continuous φ) {a : σ → R} (ha : HasEval a) : HasEval (fun s ↦ φ (a s))
    where
  hpow s := (ha.hpow s).map hφ
  tendsto_zero := (map_zero φ ▸ hφ.tendsto 0).comp ha.tendsto_zero

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