proposition: Lemma continuous_identity: forall (X:TopologicalSpace), continuous (fun x:X => x).
proof: Proof. intros. red; intros. rewrite inverse_image_id. assumption. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases