3 include "topology/igft.ma".
5 ninductive unit : Type[0] ≝ one : unit.
11 @ E (λ_.unit) (λa,x.R a);
14 unification hint 0 ≔ ;
16 (* -------------- *) ⊢
19 ndefinition emptyset: Ω^axs ≝ {x | False}.
21 ndefinition Z: Ω^axs ≝ {x | x ◃ emptyset}.
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;
30 ##[ #c; #H; napply (UV … H);
31 ##| #c; #i; #HCU; #H; napply (cinfinity … i); napply H;
35 ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
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;
44 ##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)