proposition: Lemma Ladj_continuous : forall (C D : Category) (G : Functor C D), LeftAdj G -> Continuous G.
proof: Proof. unfold Continuous, Preserves_limits in |- *; intros C D G la J H l. apply (Ladj_Pres1 la l). Defined.
imports: Adj_UA Pres_Limits