comp — Mathlib

English

If Tendsto g y z and Tendsto f x y, then Tendsto (g ∘ f) x z.

Русский

Если Tendsto g y z и Tendsto f x y, то Tendsto (g ∘ f) x z.

LaTeX

$$$\\forall f:\\alpha \\to \\beta,\\; \\forall g:\\beta \\to \\gamma,\\; \\forall x:\\mathrm{Filter}(\\alpha),\\; \\forall y:\\mathrm{Filter}(\\beta),\\; \\forall z:\\mathrm{Filter}(\\gamma),\\; (\\mathrm{Tendsto} g\\ y\\ z) \\land (\\mathrm{Tendsto} f\\ x\\ y) \\Rightarrow \\mathrm{Tendsto}(g \\circ f)\\ x\\ z$$$

Lean4

theorem comp {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} (hg : Tendsto g y z)
    (hf : Tendsto f x y) : Tendsto (g ∘ f) x z := fun _ hs => hf (hg hs)

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