---

Definition: Sierpinski-bottom
⊥ ==  λn.ff

Lemma: Sierpinski-bottom_wf
⊥ ∈ ℕ ⟶ 𝔹

Lemma: equal-Sierpinski-bottom
∀[x:ℕ ⟶ 𝔹]. uiff(x = ⊥ ∈ (ℕ ⟶ 𝔹);∀n:ℕ. (¬↑(x n)))

Definition: Sierpinski-top
⊤ ==  λn.tt

Lemma: Sierpinski-top_wf
⊤ ∈ ℕ ⟶ 𝔹

Lemma: Sierpinski-unequal-1
⊥ = ⊤ ∈ (ℕ ⟶ 𝔹) ⇐⇒ False

Lemma: two-class-equiv-rel
∀[T:Type]. ∀[t:T].  EquivRel(T;x,y.x = t ∈ T ⇐⇒ y = t ∈ T)

Definition: Sierpinski
Sierpinski ==  f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))

Lemma: Sierpinski_wf
Sierpinski ∈ Type

Lemma: subtype-Sierpinski
(ℕ ⟶ 𝔹) ⊆r Sierpinski

Lemma: not-Sierpinski-top
∀[x:Sierpinski]. ((¬(x = ⊤ ∈ Sierpinski)) ⇒ (x = ⊥ ∈ Sierpinski))

Lemma: not-Sierpinski-bottom
∀[x:Sierpinski]. ((¬(x = ⊥ ∈ Sierpinski)) ⇒ (x = ⊤ ∈ Sierpinski))

Lemma: Sierpinski-unequal
¬(⊥ = ⊤ ∈ Sierpinski)

Lemma: Sierpinski-cases
∀[x:Sierpinski]. (¬((¬(x = ⊤ ∈ Sierpinski)) ∧ (¬(x = ⊥ ∈ Sierpinski))))

Lemma: Sierpinski-cases2
∀[x:Sierpinski]. (¬¬((x = ⊤ ∈ Sierpinski) ∨ (x = ⊥ ∈ Sierpinski)))

Definition: sp-meet
f ∧ g ==  λn.let x,y = coded-pair(n) in (f x) ∧b (g y)

Lemma: sp-meet_wf
∀[f,g:Sierpinski].  (f ∧ g ∈ Sierpinski)

Definition: sp-join
f ∨ g ==  λn.((f n) ∨b(g n))

Lemma: sp-join_wf
∀[f,g:Sierpinski].  (f ∨ g ∈ Sierpinski)

Lemma: sp-meet-is-top
∀[x,y:Sierpinski].  (x ∧ y = ⊤ ∈ Sierpinski ⇐⇒ (x = ⊤ ∈ Sierpinski) ∧ (y = ⊤ ∈ Sierpinski))

Lemma: sp-join-is-bottom
∀[x,y:Sierpinski].  (x ∨ y = ⊥ ∈ Sierpinski ⇐⇒ (x = ⊥ ∈ Sierpinski) ∧ (y = ⊥ ∈ Sierpinski))

Definition: sp-lub
lub(n.A[n]) ==  λn.let i,j = coded-pair(n) in A[i] j

Lemma: sp-lub_wf1
∀[B:f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)]. (lub(n.B[n]) ∈ Sierpinski)

Lemma: sp-lub_wf
∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) ∈ Sierpinski)

Definition: sp-le
x ≤ y ==  (x = ⊤ ∈ Sierpinski) ⇒ (y = ⊤ ∈ Sierpinski)

Lemma: sp-le_wf
∀[x,y:Sierpinski].  (x ≤ y ∈ ℙ)

Lemma: sp-le_weakening
∀[x:Sierpinski]. x ≤ x

Lemma: sp-le-top
∀[x:Sierpinski]. x ≤ ⊤

Lemma: sp-le-bottom
∀[x:Sierpinski]. ⊥ ≤ x

Lemma: sp-le_transitivity
∀[x,y,z:Sierpinski].  (x ≤ y ⇒ y ≤ z ⇒ x ≤ z)

Lemma: sp-lub-is-bottom
∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) = ⊥ ∈ Sierpinski ⇐⇒ ∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski))

Lemma: sp-lub-is-top1
∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) = ⊤ ∈ Sierpinski ⇐⇒ ¬(∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski)))

Lemma: sp-lub-is-top
∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) = ⊤ ∈ Sierpinski ⇐⇒ ¬¬(∃n:ℕ. (A[n] = ⊤ ∈ Sierpinski)))

Lemma: sp-lub-property
∀[A:ℕ ⟶ Sierpinski]. ((∀n:ℕ. A[n] ≤ lub(n.A[n])) ∧ (∀c:Sierpinski. ((∀n:ℕ. A[n] ≤ c) ⇒ lub(n.A[n]) ≤ c)))

Lemma: Sierpinski-equal-bottom
∀[x:ℕ ⟶ 𝔹]. uiff(x = ⊥ ∈ Sierpinski;x = ⊥ ∈ (ℕ ⟶ 𝔹))

Lemma: Sierpinski-equal
∀[x,y:Sierpinski].  uiff(x = y ∈ Sierpinski;x = ⊥ ∈ Sierpinski ⇐⇒ y = ⊥ ∈ Sierpinski)

Lemma: Sierpinski-equal2
∀[x,y:Sierpinski].  uiff(x = y ∈ Sierpinski;x = ⊤ ∈ Sierpinski ⇐⇒ y = ⊤ ∈ Sierpinski)

Lemma: sp-meet-com
∀[x,y:Sierpinski].  (x ∧ y = y ∧ x ∈ Sierpinski)

Lemma: sp-join-com
∀[x,y:Sierpinski].  (x ∨ y = y ∨ x ∈ Sierpinski)

Lemma: sp-meet-assoc
∀[x,y,z:Sierpinski].  (x ∧ y ∧ z = x ∧ y ∧ z ∈ Sierpinski)

Lemma: sp-join-assoc
∀[x,y,z:Sierpinski].  (x ∨ y ∨ z = x ∨ y ∨ z ∈ Sierpinski)

Lemma: sp-meet-top
∀[x:Sierpinski]. (x ∧ ⊤ = x ∈ Sierpinski)

Lemma: sp-join-bottom
∀[x:Sierpinski]. (x ∨ ⊥ = x ∈ Sierpinski)

Lemma: sp-meet-bottom
∀[x:Sierpinski]. (x ∧ ⊥ = ⊥ ∈ Sierpinski)

Lemma: sp-join-top
∀[x:Sierpinski]. (x ∨ ⊤ = ⊤ ∈ Sierpinski)

Lemma: sp-join-meet-distrib
∀[x,y,z:Sierpinski].  (x ∧ y ∨ z = x ∨ z ∧ y ∨ z ∈ Sierpinski)

Lemma: sp-meet-join-distrib
∀[x,y,z:Sierpinski].  (x ∨ y ∧ z = x ∧ z ∨ y ∧ z ∈ Sierpinski)

Lemma: sp-join-idemp
∀[x:Sierpinski]. (x ∨ x = x ∈ Sierpinski)

Lemma: sp-meet-idemp
∀[x:Sierpinski]. (x ∧ x = x ∈ Sierpinski)

Definition: Open
Open(X) ==  X ⟶ Sierpinski

Lemma: Open_wf
∀[X:Type]. (Open(X) ∈ Type)

Definition: open-isect
open-isect(A;B) ==  λx.A x ∧ B x

Lemma: open-isect_wf
∀[X:Type]. ∀[A,B:Open(X)].  (open-isect(A;B) ∈ Open(X))

Definition: open-union
open-union(n.A[n]) ==  λx.lub(n.A[n] x)

Lemma: open-union_wf
∀[X:Type]. ∀[A:ℕ ⟶ Open(X)].  (open-union(n.A[n]) ∈ Open(X))

Definition: in-open
x ∈ A ==  (A x) = ⊤ ∈ Sierpinski

Lemma: in-open_wf
∀[X:Type]. ∀[x:X]. ∀[A:Open(X)].  (x ∈ A ∈ ℙ)

Lemma: in-open-isect
∀[X:Type]. ∀[x:X]. ∀[A,B:Open(X)].  (x ∈ open-isect(A;B) ⇐⇒ x ∈ A ∧ x ∈ B)

Lemma: in-open-union
∀[X:Type]. ∀[x:X]. ∀[A:ℕ ⟶ Open(X)].  (x ∈ open-union(n.A[n]) ⇐⇒ ¬¬(∃n:ℕ. ((A[n] x) = ⊤ ∈ Sierpinski)))

Definition: overt
Overt(X) ==
  ∀[Y:Type]. ∃ex:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀B:Open(Y).  (∀y:Y. ex A y ≤ B y ⇐⇒ ∀x:X. ∀y:Y.  A <x, y> ≤ B \000Cy)

Lemma: overt_wf
∀[X:Type]. (Overt(X) ∈ ℙ')

Lemma: nat-overt
Overt(ℕ)

Definition: weak-overt
wOvert(X) ==  ∀[Y:Type]. ∃f:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀y:Y.  (y ∈ f A ⇐⇒ ¬¬(∃x:X. <x, y> ∈ A))

Lemma: weak-overt_wf
∀[X:Type]. (wOvert(X) ∈ ℙ')

Lemma: weak-overt-implies-overt
∀[X:Type]. (wOvert(X) ⇒ Overt(X))

Lemma: nat-weak-overt
wOvert(ℕ)

Definition: strong-overt
sOvert(X) ==  ∀Y:Type. ∃f:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀y:Y.  (y ∈ f A ⇐⇒ ∃x:X. <x, y> ∈ A)

Lemma: strong-overt_wf
∀[X:Type]. (sOvert(X) ∈ ℙ')

Lemma: nat-strong-overt-implies-Markov
sOvert(ℕ) ⇒ (∀g:ℕ ⟶ 𝔹. ((¬(∀n:ℕ. g n = ff)) ⇒ (∃n:ℕ. g n = tt)))



Home Index