map — Mathlib

English

If x is IsSt to r and f is continuous at r, then the mapped hyperreal x.map f is IsSt to f(r).

Русский

Если x стандартен к r и f непрерывна в r, то образованный x.map f стандартен к f(r).

LaTeX

$$$\mathrm{IsSt}(x,r) \rightarrow \mathrm{ContinuousAt}(f,r) \rightarrow \mathrm{IsSt}(\mathrm{Filter.Germ.map}\ f\ x, f(r))$$$

Lean4

theorem map {x : ℝ*} {r : ℝ} (hxr : IsSt x r) {f : ℝ → ℝ} (hf : ContinuousAt f r) : IsSt (x.map f) (f r) :=
  by
  rcases ofSeq_surjective x with ⟨g, rfl⟩
  exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)

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