Nuprl Lemma : sp-lub_wf1

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


Proof




Definitions occuring in Statement :  sp-lub: lub(n.A[n]) Sierpinski: Sierpinski Sierpinski-bottom: fun-equiv: fun-equiv(X;a,b.E[a; b];f;g) quotient: x,y:A//B[x; y] nat: bool: 𝔹 uall: [x:A]. B[x] so_apply: x[s] iff: ⇐⇒ Q squash: T member: t ∈ T function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] implies:  Q Sierpinski: Sierpinski uimplies: supposing a quotient: x,y:A//B[x; y] and: P ∧ Q sp-lub: lub(n.A[n]) all: x:A. B[x] so_apply: x[s] prop: iff: ⇐⇒ Q fun-equiv: fun-equiv(X;a,b.E[a; b];f;g) uiff: uiff(P;Q) squash: T so_lambda: λ2x.t[x] rev_implies:  Q rev_uimplies: rev_uimplies(P;Q) not: ¬A false: False guard: {T}
Lemmas referenced :  fun-equiv-rel nat_wf bool_wf squash_wf iff_wf equal-wf-T-base equiv_rel_squash two-class-equiv-rel Sierpinski-bottom_wf quotient_wf quotient-member-eq coded-pair_wf equal_wf equal-Sierpinski-bottom all_wf not_wf assert_wf fun-equiv_wf equal-wf-base code-pair_wf assert_functionality_wrt_uiff coded-code-pair
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis functionEquality sqequalRule lambdaEquality hypothesisEquality baseClosed because_Cache independent_functionElimination isect_memberFormation pointwiseFunctionalityForEquality independent_isectElimination pertypeElimination productElimination dependent_functionElimination productEquality lambdaFormation spreadEquality independent_pairEquality applyEquality equalityTransitivity equalitySymmetry independent_pairFormation addLevel allFunctionality imageElimination impliesFunctionality functionExtensionality imageMemberEquality levelHypothesis promote_hyp voidElimination axiomEquality

Latex:
\mforall{}[B:f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)].  (lub(n.B[n])  \mmember{}  Sierpinski)



Date html generated: 2019_10_31-AM-06_36_00
Last ObjectModification: 2017_07_28-AM-09_12_02

Theory : synthetic!topology


Home Index