helm/software/matita/nlibrary/topology/cantor.ma

   1
   2
   3 include "topology/igft.ma".
   4
   5 ninductive unit : Type[0] ≝ one : unit.
   6
   7 naxiom E: setoid.
   8 naxiom R: E → Ω^E.
   9
  10 ndefinition axs: Ax.
  11 @ E (λ_.unit) (λa,x.R a);
  12 nqed.
  13
  14 unification hint 0 ≔ ;
  15          x ≟ axs
  16   (* -------------- *) ⊢
  17          S x ≡ E.
  18
  19 ndefinition emptyset: Ω^axs ≝ {x | False}.
  20
  21 ndefinition Z: Ω^axs ≝ {x | x ◃ emptyset}.
  22
  23 alias symbol "covers" = "covers".
  24 alias symbol "covers" = "covers set".
  25 alias symbol "covers" = "covers".
  26 alias symbol "covers" = "covers set".
  27 ntheorem cover_trans: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  28 #A; #a; #U; #V; #aU; #UV;
  29 nelim aU;
  30 ##[ #c; #H; napply (UV … H);
  31 ##| #c; #i; #HCU; #H; napply (cinfinity … i); napply H;
  32 ##]
  33 nqed.
  34
  35 ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
  36 #a; *; #ZRa; #RaZ;
  37 ncut (a ◃ R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
  38 ncut (a ◃ emptyset); ##[
  39   napply (cover_trans … H1);
  40   #x; #H; nlapply (RaZ … H); #ABS; napply ABS; ##] #H2;
  41 ncut (a ∈ R a); ##[ napply ZRa; napply H2; ##] #H3;
  42 nelim H2 in H3;
  43 ##[ nauto.
  44 ##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
  45 nqed.
  46