proposition: Lemma continuous_interior : continuous <-> forall A, Included (inverse_image f (interior A)) (interior (inverse_image f A)).
proof: Proof. split. - intros. red; intros. assert (open (inverse_image f (interior A))). { apply H. apply interior_open. } apply (interior_maximal _ _ H1). + intros ? ?. destruct H2. constructor. apply interior_deflationary. assumption. + assumption. - intros. red; intros. specialize (H V). rewrite interior_fixes_open in H; auto. assert (inverse_image f V = interior (inverse_image f V)). { apply Extensionality_Ensembles. split. - assumption. - apply interior_deflationary. } rewrite H1. apply interior_open. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases