English
If a germ f : Germ l β is constant and g: γ → α tends to l along lc, then the germ obtained by precomposing f with g is constant with respect to lc.
Русский
Если жерма f : Germ l β константна, и g: γ → α имеет предел вдоль lc к l, то жерма, полученная как композиция f ∘ g, по отношению к lc константна.
LaTeX
$$$ \\forall {f : \\mathrm{Germ}(l,\\beta)} {lc : \\mathrm{Filter}(\\gamma)} {g : \\gamma \\to \\alpha},\\ (f.IsConstant) \\land (\\mathrm{Tendsto}(g, lc, l)) \\Rightarrow (f.compTendsto g hg).IsConstant $$$
Lean4
/-- If a germ `f : Germ l β` is constant, where `l : Filter α`,
and a function `g : γ → α` tends to `l` along `lc : Filter γ`,
the germ of the composition `f ∘ g` is also constant. -/
theorem isConstant_compTendsto {f : Germ l β} {lc : Filter γ} {g : γ → α} (hf : f.IsConstant) (hg : Tendsto g lc l) :
(f.compTendsto g hg).IsConstant :=
by
induction f using Quotient.inductionOn with
| _ f => ?_
exact isConstant_comp_tendsto hf hg
