Library Hausdorff


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.

Hausdorff


Local Open Scope topology_scope.

Section hausdorff.
  Variable X : Type.
  Variable T : Topology X.

  Definition hausdorff := x y, x y
                                       Ux Uy,
                                        (Open Ux) (Open Uy)
                                         (In _ Ux x) (In _ Uy y)
                                         Disjoint _ Ux Uy.
End hausdorff.