English
If f is a germ and g is a germ α→, then composing f with g yields a germ at lc, provided g tends to l.
Русский
Если f — это зародыш, а g — зародыш функции, то композиция f ∘ g образует зародыш в lc при условии, что g стремится к l.
LaTeX
$$$ \mathrm{compTendsto}'(f) \; (g : \mathrm{Germ}(lc, \alpha)) \; (hg : g.Tendsto l) : \mathrm{Germ}(lc, \beta)$$$
Lean4
/-- Given two germs `f : Germ l β`, and `g : Germ lc α`, where `l : Filter α`, if `g` tends to `l`,
then the composition `f ∘ g` is well-defined as a germ at `lc`. -/
def compTendsto' (f : Germ l β) {lc : Filter γ} (g : Germ lc α) (hg : g.Tendsto l) : Germ lc β :=
liftOn f (fun f => g.map f) fun _f₁ _f₂ hF => inductionOn g (fun _g hg => coe_eq.2 <| hg.eventually hF) hg
