map — Mathlib

English

If φ: R → S is continuous and a ∈ R admits evaluation, then φ(a) ∈ S admits evaluation.

Русский

Если φ: R → S непрерывно, и a ∈ R имеет оценку, то φ(a) ∈ S имеет оценку.

LaTeX

$$$(\text{Continuous } \phi) \rightarrow HasEval(a) \rightarrow HasEval(\phi(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 (φ a) :=
  by
  simp only [hasEval_iff] at ha ⊢
  exact ha.map hφ

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