### Nuprl Lemma : sp-lub_wf

`∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) ∈ Sierpinski)`

Proof

Definitions occuring in Statement :  sp-lub: `lub(n.A[n])` Sierpinski: `Sierpinski` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` Sierpinski: `Sierpinski` subtype_rel: `A ⊆r B`
Lemmas referenced :  quotient-function-subtype nat_wf set_subtype_base le_wf int_subtype_base bool_wf iff_wf equal_wf Sierpinski-bottom_wf two-class-equiv-rel sp-lub_wf1 Sierpinski_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination sqequalRule intEquality lambdaEquality natural_numberEquality hypothesisEquality functionEquality independent_functionElimination applyEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A:\mBbbN{}  {}\mrightarrow{}  Sierpinski].  (lub(n.A[n])  \mmember{}  Sierpinski)

Date html generated: 2019_10_31-AM-06_36_01
Last ObjectModification: 2015_12_28-AM-11_21_20

Theory : synthetic!topology

Home Index