const_compTendsto — Mathlib

English

Precomposing a constant germ by a function g with Tendsto g lc l leaves the germ constant: the germ is unchanged by compTendsto.

Русский

Предкомпозиция константной жермы функцией g с пределом оставляет жерму константной: компоновка оставляет константную жерму без изменений.

LaTeX

$$$ (\\uparrow b : \\mathrm{Germ}(l,\\beta)).compTendsto g hg = \\uparrow b $$$

Lean4

@[simp]
theorem const_compTendsto {l : Filter α} (b : β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
    (↑b : Germ l β).compTendsto g hg = ↑b :=
  rfl

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