proposition: Lemma continuous_comp {X : UU} {U V : TopologicalSpace} (f : X → U) (g : U → V) (F : Filter X) (l : U) : is_lim f F l → continuous_at g l → is_lim (funcomp f g) F (g l).
proof: Proof. apply filterlim_comp. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures