Library TopologicalContinuity

Require Import Utf8 Setoid.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import Finite_sets Classical IndefiniteDescription.
Require Import Classes.RelationClasses Morphisms.
Require Export Topology.
Require Import Notations Common Morphism.

Set Implicit Arguments.

Generalizable All Variables.


Local Open Scope topology_scope.

Section continuous.
  Section continuous_definition.
    Variables X Y : Type.
    Variable Tx : Topology X.
    Variable Ty : Topology Y.

inverse image of open sets are open
    Definition continuous (f : XY)
      := Uy, @Open _ Ty Uy → @Open _ Tx (f -1 Uy).
  End continuous_definition.

  Section continuous_identity.
    Variable X : Type.
    Variable Tx : Topology X.
the identity function is continuous
    Definition identity_is_continuous : continuous _ _ (@id X).
      intros Uy UH.
      unfold inverse_image, id.
      match goal with
        | [ H : Open ?U |- Open ?U' ] ⇒ assert (H' : U' = U)
                                        by (apply Extensionality_Ensembles; compute; split; intro; exact id)
  End continuous_identity.

  Section continuous_composition.
    Context `(Tx : Topology X).
    Context `(Ty : Topology Y).
    Context `(Tz : Topology ZZ).

the composition of continuous functions is continuous
    Definition compose_continuous (f : YZZ) (g : XY)
    : continuous _ _ fcontinuous _ _ gcontinuous _ _ (f g).
      intros fc gc Uz UH.
      unfold continuous in ×.
      change ((f g) -1) with (g -1 f -1).
  End continuous_composition.
End continuous.