logic/equality.ma logic/connectives.ma properties/relations.ma
sets/setoids.ma logic/connectives.ma properties/relations.ma
logic/connectives.ma logic/pts.ma
+topology/cantor.ma topology/igft.ma
datatypes/pairs.ma logic/pts.ma
algebra/abelian_magmas.ma algebra/magmas.ma
nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
properties/relations1.ma logic/pts.ma
nat/big_ops.ma algebra/magmas.ma nat/order.ma
nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
+logic/destruct_bb.ma logic/equality.ma
properties/relations.ma logic/pts.ma
nat/compare.ma datatypes/bool.ma nat/order.ma
hints_declaration.ma logic/pts.ma
"sets/setoids.ma" -> "properties/relations.ma" [];
"logic/connectives.ma" [];
"logic/connectives.ma" -> "logic/pts.ma" [];
+ "topology/cantor.ma" [];
+ "topology/cantor.ma" -> "topology/igft.ma" [];
"datatypes/pairs.ma" [];
"datatypes/pairs.ma" -> "logic/pts.ma" [];
"algebra/abelian_magmas.ma" [];
"algebra/abelian_magmas.ma" -> "algebra/magmas.ma" [];
- "topology/igft-setoid.ma" [];
- "topology/igft-setoid.ma" -> "sets/sets.ma" [];
"nat/plus.ma" [];
"nat/plus.ma" -> "algebra/abelian_magmas.ma" [];
"nat/plus.ma" -> "algebra/unital_magmas.ma" [];
"nat/nat.ma" -> "hints_declaration.ma" [];
"nat/nat.ma" -> "logic/equality.ma" [];
"nat/nat.ma" -> "sets/setoids.ma" [];
+ "logic/destruct_bb.ma" [];
+ "logic/destruct_bb.ma" -> "logic/equality.ma" [];
"properties/relations.ma" [];
"properties/relations.ma" -> "logic/pts.ma" [];
"nat/compare.ma" [];
--- /dev/null
+
+
+include "topology/igft.ma".
+
+ninductive unit : Type[0] ≝ one : unit.
+
+naxiom E: setoid.
+naxiom R: E → Ω^E.
+
+ndefinition axs: Ax.
+@ E (λ_.unit) (λa,x.R a);
+nqed.
+
+unification hint 0 ≔ ;
+ x ≟ axs
+ (* -------------- *) ⊢
+ S x ≡ E.
+
+ndefinition emptyset: Ω^axs ≝ {x | False}.
+
+ndefinition Z: Ω^axs ≝ {x | x ◃ emptyset}.
+
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+ntheorem cover_trans: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+#A; #a; #U; #V; #aU; #UV;
+nelim aU;
+##[ #c; #H; napply (UV … H);
+##| #c; #i; #HCU; #H; napply (cinfinity … i); napply H;
+##]
+nqed.
+
+ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
+#a; *; #ZRa; #RaZ;
+ncut (a ◃ R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
+ncut (a ◃ emptyset); ##[
+ napply (cover_trans … H1);
+ #x; #H; nlapply (RaZ … H); #ABS; napply ABS; ##] #H2;
+ncut (a ∈ R a); ##[ napply ZRa; napply H2; ##] #H3;
+nelim H2 in H3;
+##[ nauto.
+##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+nqed.
+
D*)
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.