assumption]]
qed.
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+ (∀a:A. a ∈ U → P a) →
+ (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+ ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+ [ intros 2; simplify; apply H; assumption
+ | intros;
+ simplify in H4 ⊢ %;
+ apply H1;
+ [ apply (C ? a1 j);
+ | autobatch;
+ | assumption;
+ | assumption]]
+qed.
+
theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
intros;
cases H;
definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
-notation "↑a" with precedence 80 for @{ 'uparrow $a }.
-
interpretation "uparrow" 'uparrow a = (uparrow _ a).
-definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
-
-notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
interpretation "downarrow" 'downarrow a = (downarrow _ a).
interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
-(*
record convergent_generated_topology : Type ≝
{ AA:> axiom_set;
convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
}.
-*)