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
  17 record powerset (A: Type) : Type ≝ { char: A → CProp }.
  18
  19 interpretation "powerset" 'powerset A = (powerset A).
  20
  21 interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
  22
  23 definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
  24
  25 interpretation "mem" 'mem a S = (mem _ S a).
  26
  27 definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
  28
  29 interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
  30
  31 definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
  32
  33 interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
  34
  35 definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
  36
  37 interpretation "intersects" 'intersects U V = (intersects _ U V).
  38
  39 definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
  40
  41 interpretation "union" 'union U V = (union _ U V).
  42
  43 include "logic/equality.ma".
  44
  45 definition singleton ≝ λA:Type.λa:A.{b | a=b}.
  46
  47 interpretation "singleton" 'singl a = (singleton _ a).