const_compTendsto' — Mathlib

English

A constant germ remains invariant under precomposition with any germ g tending to l.

Русский

Константная жерма остается инвариантной при предкомпозиции с любым жермом g, стремящимся к l.

LaTeX

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

Lean4

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

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