helm/software/matita/library/datatypes/subsets.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/cprop_connectives.ma".
  16 include "datatypes/categories.ma".
  17
  18 record powerset (A: Type) : Type ≝ { char: A → CProp }.
  19
  20 interpretation "powerset" 'powerset A = (powerset A).
  21
  22 interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
  23
  24 definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
  25
  26 interpretation "mem" 'mem a S = (mem _ S a).
  27
  28 definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
  29
  30 interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
  31
  32 definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
  33
  34 interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
  35
  36 definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
  37
  38 interpretation "intersects" 'intersects U V = (intersects _ U V).
  39
  40 definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
  41
  42 interpretation "union" 'union U V = (union _ U V).
  43
  44 include "logic/equality.ma".
  45
  46 definition singleton ≝ λA:Type.λa:A.{b | a=b}.
  47
  48 interpretation "singleton" 'singl a = (singleton _ a).