compTendsto — Mathlib

English

Given a germ f and a function g that tends to l, the germ of f ∘ g is defined at lc.

Русский

Дан зародыш f и функция g, сходящаяся к l; зародыш f ∘ g определён в lc.

LaTeX

$$$ \mathrm{compTendsto}(f) \; (g : \gamma \to \alpha) \; (hg : \mathrm{Tendsto} g \ lc \ l) : \mathrm{Germ}(lc, \beta)$$$

Lean4

/-- Given a germ `f : Germ l β` and a function `g : γ → α`, where `l : Filter α`, if `g` tends
to `l` along `lc : Filter γ`, then the composition `f ∘ g` is well-defined as a germ at `lc`. -/
def compTendsto (f : Germ l β) {lc : Filter γ} (g : γ → α) (hg : Tendsto g lc l) : Germ lc β :=
  f.compTendsto' _ hg.germ_tendsto

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