English
Let l be a filter on α and f a germ in β with respect to l. If f is a constant germ and g: γ → α tends to l along the filter lc, then the germ of the composition f ∘ g with respect to lc is constant.
Русский
Пусть l — фильтр на α, а f — жерма β относительно l, являющаяся константой. Пусть g: γ → α имеет предел l вдоль фильтра lc. Тогда жерма композиции f ∘ g относительно lc константа.
LaTeX
$$$ (f : \\mathrm{Germ}(l,\\beta)).IsConstant \\land \\mathrm{Tendsto}(g, lc, l) \\Rightarrow \\mathrm{IsConstant}(f \\circ g : \\mathrm{Germ}(lc,\\beta)) $$$
Lean4
theorem isConstant_comp_tendsto {lc : Filter γ} {g : γ → α} (hf : (f : Germ l β).IsConstant) (hg : Tendsto g lc l) :
IsConstant (f ∘ g : Germ lc β) := by
rcases hf with ⟨b, hb⟩
exact ⟨b, hb.comp_tendsto hg⟩
