Nuprl Lemma : in-open-union

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


Proof




Definitions occuring in Statement :  in-open: x ∈ A open-union: open-union(n.A[n]) Open: Open(X) Sierpinski: Sierpinski Sierpinski-top: nat: uall: [x:A]. B[x] so_apply: x[s] exists: x:A. B[x] iff: ⇐⇒ Q not: ¬A apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q implies:  Q not: ¬A false: False open-union: open-union(n.A[n]) in-open: x ∈ A Open: Open(X) prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B rev_implies:  Q exists: x:A. B[x]
Lemmas referenced :  not_wf exists_wf nat_wf equal_wf Sierpinski_wf Open_wf Sierpinski-top_wf subtype-Sierpinski in-open_wf open-union_wf sp-lub-is-top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation thin sqequalHypSubstitution sqequalRule hypothesis independent_functionElimination voidElimination lemma_by_obid isectElimination lambdaEquality applyEquality hypothesisEquality because_Cache productElimination independent_pairEquality dependent_functionElimination axiomEquality functionEquality isect_memberEquality universeEquality

Latex:
\mforall{}[X:Type].  \mforall{}[x:X].  \mforall{}[A:\mBbbN{}  {}\mrightarrow{}  Open(X)].    (x  \mmember{}  open-union(n.A[n])  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  ((A[n]  x)  =  \mtop{})))



Date html generated: 2019_10_31-AM-07_19_02
Last ObjectModification: 2015_12_28-AM-11_21_48

Theory : synthetic!topology


Home Index