2 record powerset (A : Type) : Type := { content : A → CProp }.
4 notation > "Ω ^ A" non associative with precedence 50 for @{'P $A}.
5 notation "Ω \sup A" non associative with precedence 50 for @{'P $A}.
6 interpretation "Powerset" 'P A = (powerset A).
8 record AxiomSet : Type := {
14 notation "'I'" non associative with precedence 90 for @{'I}.
15 interpretation "I" 'I = (I_ _).
16 notation < "'I' \lpar a \rpar" non associative with precedence 90 for @{'I1 $a}.
17 interpretation "I a" 'I1 a = (I_ _ a).
18 notation "'C'" non associative with precedence 90 for @{'C}.
19 interpretation "C" 'C = (C_ _).
20 notation < "'C' \lpar a \rpar" non associative with precedence 90 for @{'C1 $a}.
21 interpretation "C a" 'C1 a = (C_ _ a).
22 notation < "'C' \lpar a , i \rpar" non associative with precedence 90 for @{'C2 $a $i}.
23 interpretation "C a i" 'C2 a i = (C_ _ a i).
25 definition in_subset :=
26 λA:AxiomSet.λa:A.λU:Ω^A.content A U a.
28 notation "hvbox(a break εU)" non associative with precedence 50 for
30 interpretation "In subset" 'in_subset a U = (in_subset _ a U).
32 definition for_all ≝ λA:AxiomSet.λU:Ω^A.λP:A → CProp.∀x.xεU → P x.
34 inductive covers (A : AxiomSet) (U : Ω ^ A) : A → CProp :=
35 | reflexivity : ∀a.aεU → covers A U a
36 | infinity : ∀a.∀i : I a. for_all A (C a i) (covers A U) → covers A U a.
38 notation "U ⊲ V" non associative with precedence 45
39 for @{ 'covers_subsets $U $V}.
40 interpretation "Covers subsets" 'covers_subsets U V = (for_all _ U (covers _ V)).
41 interpretation "Covers elem subset" 'covers_subsets U V = (covers _ V U).
43 definition subseteq := λA:AxiomSet.λU,V:Ω^A.∀x.xεU → xεV.
45 interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
47 definition covers_elim ≝
48 λA:AxiomSet.λU,P: Ω^A.λH1: U ⊆ P.
49 λH2:∀a:A.∀j:I a. C a j ⊲ U → C a j ⊆ P → aεP.
50 let rec aux (a:A) (p:a ⊲ U) on p : aεP ≝
51 match p return λaa.λ_:aa ⊲ U.aa ε P with
52 [ reflexivity a q ⇒ H1 a q
53 | infinity a j q ⇒ H2 a j q (λb.λr. aux b (q b r))]
57 interpretation "char" 'subset p = (mk_powerset _ p).
59 theorem transitivity: ∀A:AxiomSet.∀a:A.∀U,V. a ⊲ U → U ⊲ V → a ⊲ V.
61 apply (covers_elim ?? {a | a ⊲ V} ??? H);
62 [ intros 2; apply (H1 ? H2);
63 | intros; apply (infinity ??? j);
64 intros 2; apply (H3 ? H4);]