proposition: Lemma strong_topology_strongest: forall (T':Ensemble Y->Prop) (H1:_) (H2:_) (H3:_), (forall a:A, continuous (f a) (Y:=Build_TopologicalSpace Y T' H1 H2 H3)) -> forall V:Ensemble Y, T' V -> strong_open V.
proof: Proof. intros. unfold continuous in H. simpl in H. red; intros; apply H; trivial. Qed.
imports: TopologicalSpaces Continuity