Library OpenCover


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.

Open Covers


Local Open Scope topology_scope.

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

  Record Cover :=
    {
      CoverSets :> Ensemble (Ensemble X);
      Covers : CoverSets = Full_set _
    }.

  Definition cover_open (C : Cover) := Xj, Xj COpen Xj.

  Definition subcover (C' C : Cover) := C' C.

  Lemma open_subcover_open (C' C : Cover)
  : cover_open Csubcover C' Ccover_open C'.
  Proof.
    unfold cover_open in *;
    intuition.
  Qed.
End covers.